- Lemma ga_kappa' : ∀ Γ Δ ec l a b Σ x,
- ND Rule
- [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ]
- [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ].
- apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
- Defined.
+ Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x,
+ ND Rule
+ [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ]
+ [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply ga_first.
+
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply postcompose.
+ apply ga_uncancell.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ apply precompose.
+ Defined.