| RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁] @l] [Γ>Δ> Σ |- [σ₂ ] @l]
| RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁] @l] [Γ>Δ> Σ |- [σ₂ ] @l]
-| RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ l, Rule ([Γ > Δ > Σ₁ |- τ₁ @l],,[Γ > Δ > Σ₂ |- τ₂ @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]
| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ ]@l]
| RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@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]
| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ ]@l]
| RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l]
-| RCut : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l]
+| RCut : ∀ Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> Σ,,((Σ₁₂@@@l),,Σ₂) |- Σ₃@l ]) [Γ>Δ> Σ,,(Σ₁,,Σ₂) |- Σ₃@l]
| RLeft : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
| RRight : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
| RLeft : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
| RRight : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
[Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev]
.
[Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev]
.
+Definition RCut' : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l,
+ ND Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+ apply nd_prod.
+ apply nd_id.
+ apply nd_rule.
+ apply RArrange.
+ apply AuCanL.
+ Defined.
(* A rule is considered "flat" if it is neither RBrak nor REsc *)
(* TODO: change this to (if RBrak/REsc -> False) *)
(* A rule is considered "flat" if it is neither RBrak nor REsc *)
(* TODO: change this to (if RBrak/REsc -> False) *)
| Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 )
| Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l)
| Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l)
| Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 )
| Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l)
| Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l)
| Flat_RVoid : ∀ q a l, Rule_Flat (RVoid q a l)
| Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
| Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
| Flat_RVoid : ∀ q a l, Rule_Flat (RVoid q a l)
| Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
| Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
destruct X0; destruct s; inversion e.
destruct X0; destruct s; inversion e.
destruct X0; destruct s; inversion e.
destruct X0; destruct s; inversion e.
destruct X0; destruct s; inversion e.
destruct X0; destruct s; inversion e.
Qed.
Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
Qed.
Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.