+ End CoreToCore.
+
+ Definition coreVarToWeakExprVarOrError cv :=
+ match coreVarToWeakVar cv with
+ | WExprVar wv => wv
+ | _ => Prelude_error "IMPOSSIBLE"
+ end.
+
+ Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
+ ND Rule
+ [ Γ > Δ > Σ |- [a ---> s @@ lev ] ]
+ [ Γ > Δ > Σ,,[a @@ lev] |- [ s @@ lev ] ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
+ eapply nd_comp; [ apply nd_rlecnac | idtac ].
+ apply nd_prod.
+ apply nd_id.
+ apply nd_rule.
+ apply RVar.
+ Defined.
+
+ Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
+ ND Rule [] [ Γ > Δ > [ ] |- [a ---> s @@ lev ] ] ->
+ ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s @@ lev ] ].
+ intro pf.
+ eapply nd_comp.
+ apply pf.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+ apply curry.
+ Defined.
+
+ Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
+ ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) @@ lev ] ] ->
+ ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s @@ lev ] ].
+ intro pf.
+ eapply nd_comp.
+ eapply pf.
+ clear pf.
+ eapply nd_comp.
+ eapply curry.
+ eapply nd_comp.
+ eapply nd_rule.
+ eapply RArrange.
+ eapply RCanL.
+ apply curry.
+ Defined.
+
+ Section coqPassCoreToCore.
+ Context
+ (hetmet_brak : CoreVar)
+ (hetmet_esc : CoreVar)
+ (hetmet_flatten : CoreVar)
+ (hetmet_flattened_id : CoreVar)
+ (uniqueSupply : UniqSupply)
+ (lbinds:list (@CoreBind CoreVar))
+ (hetmet_PGArrowTyCon : TyFun)
+ (hetmet_pga_id : CoreVar)
+ (hetmet_pga_comp : CoreVar)
+ (hetmet_pga_first : CoreVar)
+ (hetmet_pga_second : CoreVar)
+ (hetmet_pga_cancell : CoreVar)
+ (hetmet_pga_cancelr : CoreVar)
+ (hetmet_pga_uncancell : CoreVar)
+ (hetmet_pga_uncancelr : CoreVar)
+ (hetmet_pga_assoc : CoreVar)
+ (hetmet_pga_unassoc : CoreVar)
+ (hetmet_pga_copy : CoreVar)
+ (hetmet_pga_drop : CoreVar)
+ (hetmet_pga_swap : CoreVar)
+ (hetmet_pga_applyl : CoreVar)
+ (hetmet_pga_applyr : CoreVar)
+ (hetmet_pga_curryl : CoreVar)
+ (hetmet_pga_curryr : CoreVar)
+ .
+
+ Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil ★ TyFunApp_nil.
+ Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
+ TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
+ Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
+ TApp (TApp (TApp (@TyFunApp TV
+ hetmet_PGArrowTyCon
+ nil _ TyFunApp_nil) a) b) c.
+ Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
+
+ Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
+ fun TV ite => TApp (TApp (TApp (@TyFunApp TV
+ hetmet_PGArrowTyCon
+ nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
+
+ Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
+ IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
+ intros.
+ inversion X; subst.
+ inversion X1; subst.
+ apply f; auto.