| 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]
| 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_RJoin : ∀ q a b c d e l, Rule_Flat (RJoin q a b c d e 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).
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.