-| RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]]
-| RLam : ∀ Γ Δ Σ tx te l, Γ ⊢ᴛy tx : ★ -> Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]]
-| RCast : ∀ Γ Δ Σ σ τ γ l, Δ ⊢ᴄᴏ γ : σ ∼ τ -> Rule [Γ>Δ> Σ |- [σ@@l] ] [Γ>Δ> Σ |- [τ @@l]]
-| RBindingGroup : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ]
-| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]]
-| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]]
-| REmptyGroup : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ]
-| RAppT : ∀ Γ Δ Σ κ σ τ l, Γ ⊢ᴛy τ : κ -> Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]]
-| RAbsT : ∀ Γ Δ Σ κ σ l,
- Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
- [Γ>Δ > Σ |- [HaskTAll κ σ @@ l]]
-| RAppCo : forall Γ Δ Σ κ σ₁ σ₂ σ γ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ ->
- Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂:κ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]]
-| RAbsCo : ∀ Γ Δ Σ κ σ σ₁ σ₂ l,
- Γ ⊢ᴛy σ₁:κ ->
- Γ ⊢ᴛy σ₂:κ ->
- Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]]
- [Γ > Δ > Σ |- [σ₁∼∼σ₂:κ⇒ σ @@l]]
-| RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ]
-| RCase : forall Γ Δ lev n tc Σ avars tbranches
- (alts:Tree ??(@ProofCaseBranch n tc Γ lev tbranches avars)),
+| RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ ] @l]
+| RGlobal : forall Γ Δ l (g:Global Γ) v, Rule [ ] [Γ>Δ> [] |- [g v ] @l]
+| RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te] @l] [Γ>Δ> Σ |- [tx--->te ] @l]
+| RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
+ HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁] @l] [Γ>Δ> Σ |- [σ₂ ] @l]
+
+(* order is important here; we want to be able to skolemize without introducing new AExch'es *)
+| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l]) [Γ>Δ> Σ₁,,Σ₂ |- [te]@l]
+
+| RCut : ∀ Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> Σ,,((Σ₁₂@@@l),,Σ₂) |- Σ₃@l ]) [Γ>Δ> Σ,,(Σ₁,,Σ₂) |- Σ₃@l]
+| RLeft : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
+| RRight : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
+
+| RVoid : ∀ Γ Δ l, Rule [] [Γ > Δ > [] |- [] @l ]
+
+| RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ]@l] [Γ>Δ> Σ |- [substT σ τ]@l]
+| RAbsT : ∀ Γ Δ Σ κ σ l n,
+ Rule [(list_ins n κ Γ)> (weakCE_ Δ) > mapOptionTree weakLT_ Σ |- [ HaskTApp (weakF_ σ) (FreshHaskTyVar_ _) ]@(weakL_ l)]
+ [Γ>Δ > Σ |- [HaskTAll κ σ ]@l]
+
+| RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
+ Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ]@l] [Γ>Δ> Σ |- [σ ]@l]
+| RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
+ Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ ]@l]
+ [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ ]@l]
+
+| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > (τ₂@@@lev),,Σ₁ |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
+| RCase : forall Γ Δ lev tc Σ avars tbranches
+ (alts:Tree ??( (@StrongAltCon tc) * (Tree ??(LeveledHaskType Γ ★)) )),