src/HaskFlattener.v

   1 (*********************************************************************************************************************************)
   2 (* HaskFlattener:                                                                                                                *)
   3 (*                                                                                                                               *)
   4 (*    The Flattening Functor.                                                                                                    *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12 Require Import NaturalDeductionContext.
  13 Require Import Coq.Strings.String.
  14 Require Import Coq.Lists.List.
  15
  16 Require Import HaskKinds.
  17 Require Import HaskCoreTypes.
  18 Require Import HaskCoreVars.
  19 Require Import HaskWeakTypes.
  20 Require Import HaskWeakVars.
  21 Require Import HaskLiterals.
  22 Require Import HaskTyCons.
  23 Require Import HaskStrongTypes.
  24 Require Import HaskProof.
  25 Require Import NaturalDeduction.
  26
  27 Require Import HaskStrongTypes.
  28 Require Import HaskStrong.
  29 Require Import HaskProof.
  30 Require Import HaskStrongToProof.
  31 Require Import HaskProofToStrong.
  32 Require Import HaskWeakToStrong.
  33
  34 Require Import HaskSkolemizer.
  35
  36 Open Scope nd_scope.
  37 Set Printing Width 130.
  38
  39 (*
  40  *  The flattening transformation.  Currently only TWO-level languages are
  41  *  supported, and the level-1 sublanguage is rather limited.
  42  *
  43  *  This file abuses terminology pretty badly.  For purposes of this file,
  44  *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
  45  *  the whole language (level-0 language including bracketed level-1 terms)
  46  *)
  47 Section HaskFlattener.
  48
  49
  50   Ltac eqd_dec_refl' :=
  51     match goal with
  52       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
  53         destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
  54           [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
  55   end.
  56
  57   Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
  58
  59   Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
  60     fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
  61
  62   (* In a tree of types, replace any type at depth "lev" or greater None *)
  63   Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
  64     mkFlags (liftBoolFunc false (levelMatch lev)) tt.
  65
  66   Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
  67     dropT (mkDropFlags lev tt).
  68
  69   (* The opposite: replace any type which is NOT at level "lev" with None *)
  70   Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
  71     mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
  72
  73   Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
  74     dropT (mkTakeFlags lev tt).
  75 (*
  76     mapOptionTree (fun x => flatten_type (unlev x))
  77     (maybeTree (takeT tt (mkFlags (
  78       fun t => match t with
  79                  | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
  80                  | _                    => true
  81                end
  82     ) tt))).
  83
  84   Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
  85     match t with
  86       | None   => []
  87       | Some x => x
  88     end.
  89 *)
  90
  91   Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@  lev] = [].
  92     intros; simpl.
  93     Opaque eqd_dec.
  94     unfold drop_lev.
  95     simpl.
  96     unfold mkDropFlags.
  97     simpl.
  98     Transparent eqd_dec.
  99     eqd_dec_refl'.
 100     auto.
 101     Qed.
 102
 103   Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@  (ec :: lev)] = [].
 104     intros; simpl.
 105     Opaque eqd_dec.
 106     unfold drop_lev.
 107     unfold mkDropFlags.
 108     simpl.
 109     Transparent eqd_dec.
 110     eqd_dec_refl'.
 111     auto.
 112     Qed.
 113
 114   Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@  lev] = [x @@ lev].
 115     intros; simpl.
 116     Opaque eqd_dec.
 117     unfold take_lev.
 118     unfold mkTakeFlags.
 119     simpl.
 120     Transparent eqd_dec.
 121     eqd_dec_refl'.
 122     auto.
 123     Qed.
 124
 125   Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev.
 126     intros.
 127     induction x.
 128     destruct a; simpl; try reflexivity.
 129     apply take_lemma.
 130     simpl.
 131     rewrite <- IHx1 at 2.
 132     rewrite <- IHx2 at 2.
 133     reflexivity.
 134     Qed.
 135
 136   Ltac drop_simplify :=
 137     match goal with
 138       | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 139         rewrite (drop_lev_lemma G L X)
 140       | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
 141         rewrite (drop_lev_lemma_s G L E X)
 142       | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
 143       change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
 144       | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
 145       change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 146     end.
 147
 148   Ltac take_simplify :=
 149     match goal with
 150       | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 151         rewrite (take_lemma G L X)
 152       | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
 153         rewrite (take_lemma' G L X)
 154       | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
 155       change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
 156       | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
 157       change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 158     end.
 159
 160
 161   (*******************************************************************************)
 162
 163
 164   Context {unitTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★                                          }.
 165   Context {prodTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
 166   Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
 167
 168   Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
 169     reduceTree (unitTy TV ec) (prodTy TV ec) tr.
 170
 171   Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 172     fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
 173
 174   Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
 175     gaTy TV ec
 176     (ga_mk_tree' ec ant)
 177     (ga_mk_tree' ec suc).
 178
 179   Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 180     fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
 181
 182   (*
 183    *  The story:
 184    *    - code types <[t]>@c                                                become garrows  c () t
 185    *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
 186    *    - free variables at the level of the succedent become
 187    *)
 188   Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
 189     match exp with
 190     | TVar    _  x          => TVar x
 191     | TAll     _ y          => TAll   _  (fun v => flatten_rawtype (y v))
 192     | TApp   _ _ x y        => TApp      (flatten_rawtype x) (flatten_rawtype y)
 193     | TCon       tc         => TCon      tc
 194     | TCoerc _ t1 t2 t      => TCoerc    (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
 195     | TArrow                => TArrow
 196     | TCode     ec e        => let e' := flatten_rawtype e
 197                                in  ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
 198     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
 199     end
 200     with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
 201     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
 202     | TyFunApp_nil               => TyFunApp_nil
 203     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
 204     end.
 205
 206   Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
 207     fun TV ite => flatten_rawtype (ht TV ite).
 208
 209   Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
 210     match lev with
 211       | nil      => flatten_type ht
 212       | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
 213     end.
 214
 215   Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
 216     levels_to_tcode (unlev ht) (getlev ht) @@ nil.
 217
 218   (* AXIOMS *)
 219
 220   Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
 221
 222   Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
 223     HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
 224
 225   Axiom flatten_commutes_with_substT :
 226     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
 227     flatten_type  (substT σ τ) = substT (fun TV ite v => flatten_rawtype  (σ TV ite v))
 228       (flatten_type  τ).
 229
 230   Axiom flatten_commutes_with_HaskTAll :
 231     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 232     flatten_type  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
 233
 234   Axiom flatten_commutes_with_HaskTApp :
 235     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 236     flatten_type  (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
 237     HaskTApp (weakF (fun TV ite v => flatten_rawtype  (σ TV ite v))) (FreshHaskTyVar κ).
 238
 239   Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ  t,
 240     flatten_leveled_type  (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type  t).
 241
 242   Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
 243     flatten_type (g v) = g v.
 244
 245   (* "n" is the maximum depth remaining AFTER flattening *)
 246   Definition flatten_judgment (j:Judg) :=
 247     match j as J return Judg with
 248       | Γ > Δ > ant |- suc @ nil        => Γ > Δ > mapOptionTree flatten_leveled_type ant
 249                                                 |- mapOptionTree flatten_type suc @ nil
 250       | Γ > Δ > ant |- suc @ (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
 251                                                 |- [ga_mk (v2t ec)
 252                                                   (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
 253                                                   (mapOptionTree  flatten_type                               suc )
 254                                                   ] @ nil
 255     end.
 256
 257   Class garrow :=
 258   { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a a ]@l ]
 259   ; ga_cancelr   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,[]) a ]@l ]
 260   ; ga_cancell   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ([],,a) a ]@l ]
 261   ; ga_uncancelr : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,[]) ]@l ]
 262   ; ga_uncancell : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a ([],,a) ]@l ]
 263   ; ga_assoc     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) ]@l ]
 264   ; ga_unassoc   : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) ]@l ]
 265   ; ga_swap      : ∀ Γ Δ ec l a b  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,b) (b,,a) ]@l ]
 266   ; ga_drop      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a [] ]@l ]
 267   ; ga_copy      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,a) ]@l ]
 268   ; ga_first     : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (a,,x) (b,,x) ]@l ]
 269   ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ]
 270   ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ]
 271   ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ]
 272   ; ga_loopl     : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (z,,x) (z,,y) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
 273   ; ga_loopr     : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (x,,z) (y,,z) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
 274   ; ga_comp      : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c ]@l ]
 275   ; ga_apply     : ∀ Γ Δ ec l a a' b c,
 276                  ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
 277   ; ga_kappa     : ∀ Γ Δ ec l a b c Σ, ND Rule
 278   [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec b c      ]@l ]
 279   [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,b) c ]@l ]
 280   }.
 281   Context `(gar:garrow).
 282
 283   Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
 284
 285   Definition boost : forall Γ Δ ant x y {lev},
 286     ND Rule []                         [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
 287     ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant      |- [y]@lev ].
 288     intros.
 289     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 290     eapply nd_comp; [ idtac | apply RLet ].
 291     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 292     apply nd_prod.
 293     apply nd_id.
 294     eapply nd_comp.
 295       apply X.
 296       eapply nd_rule.
 297       eapply RArrange.
 298       apply AuCanR.
 299     Defined.
 300
 301   Definition precompose Γ Δ ec : forall a x y z lev,
 302     ND Rule
 303       [ Γ > Δ > a                           |- [@ga_mk _ ec y z ]@lev ]
 304       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 305     intros.
 306     eapply nd_comp; [ idtac | eapply RLet ].
 307     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 308     apply nd_prod.
 309     apply nd_id.
 310     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 311     apply ga_comp.
 312     Defined.
 313
 314   Definition precompose' Γ Δ ec : forall a b x y z lev,
 315     ND Rule
 316       [ Γ > Δ > a,,b                             |- [@ga_mk _ ec y z ]@lev ]
 317       [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
 318     intros.
 319     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
 320     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
 321     apply precompose.
 322     Defined.
 323
 324   Definition postcompose_ Γ Δ ec : forall a x y z lev,
 325     ND Rule
 326       [ Γ > Δ > a                           |- [@ga_mk _ ec x y ]@lev ]
 327       [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 328     intros.
 329     eapply nd_comp; [ idtac | eapply RLet ].
 330     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 331     apply nd_prod.
 332     apply nd_id.
 333     apply ga_comp.
 334     Defined.
 335
 336   Definition postcompose  Γ Δ ec : forall x y z lev,
 337     ND Rule [] [ Γ > Δ > []                       |- [@ga_mk _ ec x y ]@lev ] ->
 338     ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 339     intros.
 340     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
 341     eapply nd_comp; [ idtac | eapply postcompose_ ].
 342     apply X.
 343     Defined.
 344
 345   Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
 346     ND Rule [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
 347             [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
 348     intros.
 349     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 350     eapply nd_comp; [ idtac | apply RLet ].
 351     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 352     apply nd_prod.
 353     apply nd_id.
 354     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
 355     apply ga_first.
 356     Defined.
 357
 358   Definition firstify : ∀ Γ Δ ec lev a b c Σ,
 359     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ] ->
 360     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
 361     intros.
 362     eapply nd_comp.
 363     apply X.
 364     apply first_nd.
 365     Defined.
 366
 367   Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
 368      ND Rule
 369      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
 370      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
 371     intros.
 372     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 373     eapply nd_comp; [ idtac | apply RLet ].
 374     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 375     apply nd_prod.
 376     apply nd_id.
 377     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
 378     apply ga_second.
 379     Defined.
 380
 381   Definition secondify : ∀ Γ Δ ec lev a b c Σ,
 382      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ] ->
 383      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
 384     intros.
 385     eapply nd_comp.
 386     apply X.
 387     apply second_nd.
 388     Defined.
 389
 390    Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ x,
 391      ND Rule
 392      [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b ]@l ]
 393      [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x       b ]@l ].
 394      intros.
 395      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 396      eapply nd_comp; [ idtac | eapply RLet ].
 397      eapply nd_comp; [ apply nd_llecnac | idtac ].
 398      apply nd_prod.
 399      apply ga_first.
 400
 401      eapply nd_comp; [ idtac | eapply RLet ].
 402      eapply nd_comp; [ apply nd_llecnac | idtac ].
 403      apply nd_prod.
 404      apply postcompose.
 405      apply ga_uncancell.
 406      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 407      apply precompose.
 408      Defined.
 409
 410   (* useful for cutting down on the pretty-printed noise
 411
 412   Notation "`  x" := (take_lev _ x) (at level 20).
 413   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 414   Notation "``` x" := (drop_lev _ x) (at level 20).
 415   *)
 416   Definition flatten_arrangement' :
 417     forall Γ (Δ:CoercionEnv Γ)
 418       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 419       ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 420         (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
 421
 422       intros Γ Δ ec lev.
 423       refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
 424            ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 425              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 426              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
 427         match r as R in Arrange A B return
 428           ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 429             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
 430             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
 431           with
 432           | AId  a               => let case_AId := tt    in ga_id _ _ _ _ _
 433           | ACanL  a             => let case_ACanL := tt  in ga_uncancell _ _ _ _ _
 434           | ACanR  a             => let case_ACanR := tt  in ga_uncancelr _ _ _ _ _
 435           | AuCanL a             => let case_AuCanL := tt in ga_cancell _ _ _ _ _
 436           | AuCanR a             => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
 437           | AAssoc a b c         => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
 438           | AuAssoc a b c         => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
 439           | AExch  a b           => let case_AExch := tt  in ga_swap  _ _ _ _ _ _
 440           | AWeak  a             => let case_AWeak := tt  in ga_drop _ _ _ _ _
 441           | ACont  a             => let case_ACont := tt  in ga_copy  _ _ _ _ _
 442           | ALeft  a b c r'      => let case_ALeft := tt  in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 443           | ARight a b c r'      => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 444           | AComp  c b a r1 r2   => let case_AComp := tt  in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
 445         end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 446
 447         destruct case_AComp.
 448           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
 449           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
 450           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
 451           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
 452           eapply nd_comp; [ idtac | apply
 453              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
 454           eapply nd_comp; [ apply nd_llecnac | idtac ].
 455           apply nd_prod.
 456           apply r2'.
 457           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
 458           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
 459           eapply nd_comp; [ idtac | apply RLet ].
 460           eapply nd_comp; [ apply nd_llecnac | idtac ].
 461           eapply nd_prod.
 462           apply r1'.
 463           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 464           apply ga_comp.
 465           Defined.
 466
 467   Definition flatten_arrangement :
 468     forall Γ (Δ:CoercionEnv Γ) n
 469       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 470       ND Rule
 471       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
 472         |- [@ga_mk _ (v2t ec)
 473           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
 474           (mapOptionTree (flatten_type ) succ) ]@nil]
 475       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
 476         |- [@ga_mk _ (v2t ec)
 477           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 478           (mapOptionTree (flatten_type ) succ) ]@nil].
 479       intros.
 480       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 481       apply nd_rule.
 482       apply RArrange.
 483       refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
 484         match r as R in Arrange A B return
 485           Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
 486           (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
 487           | AId  a               => let case_AId := tt  in AId _
 488           | ACanL  a             => let case_ACanL := tt  in ACanL _
 489           | ACanR  a             => let case_ACanR := tt  in ACanR _
 490           | AuCanL a             => let case_AuCanL := tt in AuCanL _
 491           | AuCanR a             => let case_AuCanR := tt in AuCanR _
 492           | AAssoc a b c         => let case_AAssoc := tt in AAssoc _ _ _
 493           | AuAssoc a b c         => let case_AuAssoc := tt in AuAssoc _ _ _
 494           | AExch  a b           => let case_AExch := tt  in AExch _ _
 495           | AWeak  a             => let case_AWeak := tt  in AWeak _
 496           | ACont  a             => let case_ACont := tt  in ACont _
 497           | ALeft  a b c r'      => let case_ALeft := tt  in ALeft  _ (flatten _ _ r')
 498           | ARight a b c r'      => let case_ARight := tt in ARight _ (flatten _ _ r')
 499           | AComp  a b c r1 r2   => let case_AComp := tt  in AComp    (flatten _ _ r1) (flatten _ _ r2)
 500         end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 501         Defined.
 502
 503   Definition flatten_arrangement'' :
 504     forall  Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
 505       ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
 506       (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
 507     intros.
 508     simpl.
 509     destruct l.
 510       apply nd_rule.
 511       apply RArrange.
 512       induction r; simpl.
 513         apply AId.
 514         apply ACanL.
 515         apply ACanR.
 516         apply AuCanL.
 517         apply AuCanR.
 518         apply AAssoc.
 519         apply AuAssoc.
 520         apply AExch.    (* TO DO: check for all-leaf trees here *)
 521         apply AWeak.
 522         apply ACont.
 523         apply ALeft; auto.
 524         apply ARight; auto.
 525         eapply AComp; [ apply IHr1 | apply IHr2 ].
 526
 527       apply flatten_arrangement.
 528         apply r.
 529         Defined.
 530
 531   Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
 532     ND Rule [] [Γ > Δ > Σ₁     |- [@ga_mk _ ec [] a      ]@nil] ->
 533     ND Rule [] [Γ > Δ > Σ₂     |- [@ga_mk _ ec [] b      ]@nil] ->
 534     ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil].
 535     intro pfa.
 536     intro pfb.
 537     apply secondify with (c:=a)  in pfb.
 538     apply firstify  with (c:=[])  in pfa.
 539     eapply nd_comp; [ idtac | eapply RLet ].
 540     eapply nd_comp; [ eapply nd_llecnac | idtac ].
 541     apply nd_prod.
 542     apply pfa.
 543     clear pfa.
 544
 545     eapply nd_comp; [ idtac | eapply RLet ].
 546     eapply nd_comp; [ apply nd_llecnac | idtac ].
 547     apply nd_prod.
 548     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
 549     eapply nd_comp; [ idtac | eapply postcompose_ ].
 550     apply ga_uncancelr.
 551
 552     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 553     eapply nd_comp; [ idtac | eapply precompose ].
 554     apply pfb.
 555     Defined.
 556
 557   Definition arrange_brak : forall Γ Δ ec succ t,
 558    ND Rule
 559      [Γ > Δ >
 560       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
 561       mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]
 562      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil].
 563
 564     intros.
 565     unfold drop_lev.
 566     set (@arrangeUnPartition _ succ (levelMatch (ec::nil))) as q.
 567     set (arrangeMap _ _ flatten_leveled_type q) as y.
 568     eapply nd_comp.
 569     Focus 2.
 570     eapply nd_rule.
 571     eapply RArrange.
 572     apply y.
 573     idtac.
 574     clear y q.
 575     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 576     simpl.
 577     eapply nd_comp; [ apply nd_llecnac | idtac ].
 578     eapply nd_comp; [ idtac | eapply RLet ].
 579     apply nd_prod.
 580     Focus 2.
 581     apply nd_id.
 582     idtac.
 583     induction succ; try destruct a; simpl.
 584     unfold take_lev.
 585     unfold mkTakeFlags.
 586     unfold mkFlags.
 587     unfold bnot.
 588     simpl.
 589     destruct l as [t' lev'].
 590     destruct lev' as [|ec' lev'].
 591     simpl.
 592     apply ga_id.
 593     unfold levelMatch.
 594     set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
 595     destruct q.
 596     inversion e; subst.
 597     simpl.
 598     apply nd_rule.
 599     unfold flatten_leveled_type.
 600     simpl.
 601     unfold flatten_type.
 602     simpl.
 603     unfold ga_mk.
 604     simpl.
 605     apply RVar.
 606     simpl.
 607     apply ga_id.
 608     apply ga_id.
 609     unfold take_lev.
 610     simpl.
 611     apply ga_join.
 612       apply IHsucc1.
 613       apply IHsucc2.
 614     Defined.
 615
 616   Definition arrange_esc : forall Γ Δ ec succ t,
 617    ND Rule
 618      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
 619      [Γ > Δ >
 620       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
 621       mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ)  |- [t]@nil].
 622     intros.
 623     set (@arrangePartition _ succ (levelMatch (ec::nil))) as q.
 624     set (@drop_lev Γ (ec::nil) succ) as q'.
 625     assert (@drop_lev Γ (ec::nil) succ=q') as H.
 626       reflexivity.
 627     unfold drop_lev in H.
 628     unfold mkDropFlags in H.
 629     rewrite H in q.
 630     clear H.
 631     set (arrangeMap _ _ flatten_leveled_type q) as y.
 632     eapply nd_comp.
 633     eapply nd_rule.
 634     eapply RArrange.
 635     apply y.
 636     clear y q.
 637
 638     set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
 639     destruct (decide_tree_empty q).
 640
 641       destruct s.
 642       simpl.
 643       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
 644       set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
 645       eapply nd_comp; [ idtac | apply RLet ].
 646       clear q''.
 647       eapply nd_comp; [ apply nd_rlecnac | idtac ].
 648       apply nd_prod.
 649       apply nd_rule.
 650       apply RArrange.
 651       eapply AComp; [ idtac | apply ACanR ].
 652       apply ALeft.
 653       apply (@arrangeCancelEmptyTree _ _ _ _ e).
 654
 655       eapply nd_comp.
 656         eapply nd_rule.
 657         eapply (@RVar Γ Δ t nil).
 658       apply nd_rule.
 659         apply RArrange.
 660         eapply AComp.
 661         apply AuCanR.
 662         apply ALeft.
 663         apply AWeak.
 664
 665       simpl.
 666       clear q.
 667       unfold q'.
 668       clear q'.
 669       apply nd_rule.
 670       apply RArrange.
 671       induction succ.
 672       destruct a.
 673       destruct l as [t' l'].
 674       simpl.
 675       Transparent drop_lev.
 676       simpl.
 677       unfold take_lev.
 678       unfold mkTakeFlags.
 679       simpl.
 680       unfold drop_lev.
 681       simpl.
 682       unfold mkDropFlags.
 683       simpl.
 684       unfold flatten_leveled_type.
 685       destruct (General.list_eq_dec l' (ec :: nil)); simpl.
 686       rewrite e.
 687       unfold levels_to_tcode.
 688       eapply AComp.
 689       apply ACanL.
 690       apply AuCanR.
 691       eapply AComp.
 692       apply ACanR.
 693       eapply AComp.
 694       apply AuCanL.
 695       apply ARight.
 696       apply AWeak.
 697
 698       simpl.
 699       apply ARight.
 700       apply AWeak.
 701
 702       drop_simplify.
 703       simpl.
 704       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ2)) as d2 in *.
 705       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ1)) as d1 in *.
 706       set (mapOptionTree flatten_leveled_type (dropT (mkFlags
 707         (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ1))) as s1 in *.
 708       set (mapOptionTree flatten_leveled_type (dropT (mkFlags
 709         (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ2))) as s2 in *.
 710       set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
 711         (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ1))) as s1' in *.
 712       set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
 713         (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ2))) as s2' in *.
 714
 715       eapply AComp.
 716       apply arrangeSwapMiddle.
 717
 718       eapply AComp.
 719       eapply ALeft.
 720       apply IHsucc2.
 721
 722       eapply AComp.
 723       eapply ARight.
 724       apply IHsucc1.
 725
 726       eapply AComp.
 727       apply arrangeSwapMiddle.
 728       apply ARight.
 729       unfold take_lev.
 730       unfold mkTakeFlags.
 731
 732       unfold s1'.
 733       unfold s2'.
 734       clear s1' s2'.
 735       set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
 736         (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ1))) as s1' in *.
 737       set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
 738         (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ2))) as s2' in *.
 739
 740       apply (Prelude_error "almost there!").
 741     Defined.
 742
 743   Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
 744     intros.
 745     induction t.
 746     destruct a; reflexivity.
 747     rewrite <- IHt1 at 2.
 748     rewrite <- IHt2 at 2.
 749     reflexivity.
 750     Qed.
 751
 752   Lemma tree_of_nothing : forall Γ ec t,
 753     Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
 754     intros.
 755     induction t; try destruct o; try destruct a.
 756     simpl.
 757     drop_simplify.
 758     simpl.
 759     apply AId.
 760     simpl.
 761     apply AId.
 762     eapply AComp; [ idtac | apply ACanL ].
 763     eapply AComp; [ idtac | eapply ALeft; apply IHt2 ].
 764     Opaque drop_lev.
 765     simpl.
 766     Transparent drop_lev.
 767     idtac.
 768     drop_simplify.
 769     apply ARight.
 770     apply IHt1.
 771     Defined.
 772
 773   Lemma tree_of_nothing' : forall Γ ec t,
 774     Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
 775     intros.
 776     induction t; try destruct o; try destruct a.
 777     simpl.
 778     drop_simplify.
 779     simpl.
 780     apply AId.
 781     simpl.
 782     apply AId.
 783     eapply AComp; [ apply AuCanL | idtac ].
 784     eapply AComp; [ eapply ARight; apply IHt1 | idtac ].
 785     Opaque drop_lev.
 786     simpl.
 787     Transparent drop_lev.
 788     idtac.
 789     drop_simplify.
 790     apply ALeft.
 791     apply IHt2.
 792     Defined.
 793
 794   Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
 795     flatten_type (<[ ec |- t ]>)
 796     = @ga_mk Γ (v2t ec)
 797     (mapOptionTree flatten_type (take_arg_types_as_tree t))
 798     [ flatten_type (drop_arg_types_as_tree   t)].
 799     intros.
 800     unfold flatten_type at 1.
 801     simpl.
 802     unfold ga_mk.
 803     apply phoas_extensionality.
 804     intros.
 805     unfold v2t.
 806     unfold ga_mk_raw.
 807     unfold ga_mk_tree.
 808     rewrite <- mapOptionTree_compose.
 809     unfold take_arg_types_as_tree.
 810     simpl.
 811     replace (flatten_type (drop_arg_types_as_tree t) tv ite)
 812       with (drop_arg_types (flatten_rawtype (t tv ite))).
 813     replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
 814       with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
 815            (unleaves_
 816               (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
 817                  (fun TV : Kind → Type => take_arg_types ○ t TV))))).
 818     reflexivity.
 819     unfold flatten_type.
 820     clear gar.
 821     set (t tv ite) as x.
 822     admit.
 823     admit.
 824     Qed.
 825
 826   Lemma drop_to_nothing : forall (Γ:TypeEnv) Σ (lev:HaskLevel Γ),
 827     drop_lev lev (Σ @@@ lev) = mapTree (fun _ => None) (mapTree (fun _ => tt) Σ).
 828     intros.
 829     induction Σ.
 830     destruct a; simpl.
 831     drop_simplify.
 832     auto.
 833     drop_simplify.
 834     auto.
 835     simpl.
 836     rewrite <- IHΣ1.
 837     rewrite <- IHΣ2.
 838     reflexivity.
 839     Qed.
 840
 841   Definition flatten_skolemized_proof :
 842     forall  {h}{c},
 843       ND SRule h c ->
 844       ND  Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
 845     intros.
 846     eapply nd_map'; [ idtac | apply X ].
 847     clear h c X.
 848     intros.
 849     simpl in *.
 850
 851     refine
 852       (match X as R in SRule H C with
 853       | SBrak    Γ Δ t ec succ lev           => let case_SBrak := tt         in _
 854       | SEsc     Γ Δ t ec succ lev           => let case_SEsc := tt          in _
 855       | SFlat    h c r                       => let case_SFlat := tt         in _
 856       end).
 857
 858     destruct case_SFlat.
 859     refine (match r as R in Rule H C with
 860       | RArrange Γ Δ a b x l d         => let case_RArrange := tt      in _
 861       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 862       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 863       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 864       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 865       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 866       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 867       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 868       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 869       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 870       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 871       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 872       | RCut     Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
 873       | RLeft    Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
 874       | RRight   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
 875       | RVoid    _ _       l           => let case_RVoid := tt   in _
 876       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 877       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 878       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 879       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 880       end); clear X h c.
 881
 882     destruct case_RArrange.
 883       apply (flatten_arrangement''  Γ Δ a b x _ d).
 884
 885     destruct case_RBrak.
 886       apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
 887
 888     destruct case_REsc.
 889       apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
 890
 891     destruct case_RNote.
 892       simpl.
 893       destruct l; simpl.
 894         apply nd_rule; apply RNote; auto.
 895         apply nd_rule; apply RNote; auto.
 896
 897     destruct case_RLit.
 898       simpl.
 899       destruct l0; simpl.
 900         unfold flatten_leveled_type.
 901         simpl.
 902         rewrite literal_types_unchanged.
 903           apply nd_rule; apply RLit.
 904         unfold take_lev; simpl.
 905         unfold drop_lev; simpl.
 906         simpl.
 907         rewrite literal_types_unchanged.
 908         apply ga_lit.
 909
 910     destruct case_RVar.
 911       Opaque flatten_judgment.
 912       simpl.
 913       Transparent flatten_judgment.
 914       idtac.
 915       unfold flatten_judgment.
 916       destruct lev.
 917       apply nd_rule. apply RVar.
 918       repeat drop_simplify.
 919       repeat take_simplify.
 920       simpl.
 921       apply ga_id.
 922
 923     destruct case_RGlobal.
 924       simpl.
 925       rename l into g.
 926       rename σ into l.
 927       destruct l as [|ec lev]; simpl.
 928         (*
 929         destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
 930           set (flatten_type (g wev)) as t.
 931           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 932           simpl in q.
 933           apply nd_rule.
 934           apply q.
 935           apply INil.
 936         destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
 937           set (flatten_type (g wev)) as t.
 938           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 939           simpl in q.
 940           apply nd_rule.
 941           apply q.
 942           apply INil.
 943           *)
 944         unfold flatten_leveled_type. simpl.
 945           apply nd_rule; rewrite globals_do_not_have_code_types.
 946           apply RGlobal.
 947       apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
 948
 949     destruct case_RLam.
 950       Opaque drop_lev.
 951       Opaque take_lev.
 952       simpl.
 953       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 954       repeat drop_simplify.
 955       repeat take_simplify.
 956       eapply nd_comp.
 957         eapply nd_rule.
 958         eapply RArrange.
 959         simpl.
 960         apply ACanR.
 961       apply boost.
 962       simpl.
 963       apply ga_curry.
 964
 965     destruct case_RCast.
 966       simpl.
 967       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 968       simpl.
 969       apply flatten_coercion; auto.
 970       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 971
 972     destruct case_RApp.
 973       simpl.
 974
 975       destruct lev as [|ec lev].
 976         unfold flatten_type at 1.
 977         simpl.
 978         apply nd_rule.
 979         apply RApp.
 980
 981         repeat drop_simplify.
 982           repeat take_simplify.
 983           rewrite mapOptionTree_distributes.
 984           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
 985           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
 986           set (take_lev (ec :: lev) Σ₁) as Σ₁''.
 987           set (take_lev (ec :: lev) Σ₂) as Σ₂''.
 988           replace (flatten_type  (tx ---> te)) with ((flatten_type  tx) ---> (flatten_type  te)).
 989           apply (Prelude_error "FIXME: ga_apply").
 990           reflexivity.
 991
 992 (*
 993   Notation "`  x" := (take_lev _ x).
 994   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 995   Notation "``` x" := ((drop_lev _ x)) (at level 20).
 996   Notation "!<[]> x" := (flatten_type _ x) (at level 1).
 997   Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
 998 *)
 999
1000     destruct case_RCut.
1001       simpl.
1002       destruct l as [|ec lev]; simpl.
1003         apply nd_rule.
1004         replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
1005         apply RCut.
1006         induction Σ₁₂; try destruct a; auto.
1007         simpl.
1008         rewrite <- IHΣ₁₂1.
1009         rewrite <- IHΣ₁₂2.
1010         reflexivity.
1011       simpl; repeat drop_simplify.
1012       simpl; repeat take_simplify.
1013       simpl.
1014       set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
1015       rewrite take_lemma'.
1016       rewrite mapOptionTree_compose.
1017       rewrite mapOptionTree_compose.
1018       rewrite mapOptionTree_compose.
1019       rewrite mapOptionTree_compose.
1020       rewrite unlev_relev.
1021       rewrite <- mapOptionTree_compose.
1022       rewrite <- mapOptionTree_compose.
1023       rewrite <- mapOptionTree_compose.
1024       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1025       apply nd_prod.
1026       apply nd_id.
1027       eapply nd_comp.
1028       eapply nd_rule.
1029       eapply RArrange.
1030       eapply ALeft.
1031       eapply ARight.
1032       unfold x1.
1033       rewrite drop_to_nothing.
1034       apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
1035         induction Σ₁₂; try destruct a; auto.
1036         simpl.
1037         rewrite <- IHΣ₁₂1 at 2.
1038         rewrite <- IHΣ₁₂2 at 2.
1039         reflexivity.
1040       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ].
1041       set (mapOptionTree flatten_type Σ₁₂) as a.
1042       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
1043       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
1044       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
1045       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ)) as e.
1046       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ)) as f.
1047       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1048       eapply nd_comp; [ apply nd_llecnac | idtac ].
1049       apply nd_prod.
1050       simpl.
1051       eapply secondify.
1052       apply ga_first.
1053       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
1054       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
1055       simpl.
1056       apply precompose.
1057
1058     destruct case_RLeft.
1059       simpl.
1060       destruct l as [|ec lev].
1061       simpl.
1062         replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1063         apply nd_rule.
1064         apply RLeft.
1065         induction Σ; try destruct a; auto.
1066         simpl.
1067         rewrite <- IHΣ1.
1068         rewrite <- IHΣ2.
1069         reflexivity.
1070       repeat drop_simplify.
1071         rewrite drop_to_nothing.
1072         simpl.
1073         eapply nd_comp.
1074         Focus 2.
1075         eapply nd_rule.
1076         eapply RArrange.
1077         eapply ARight.
1078         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1079           induction Σ; try destruct a; auto.
1080           simpl.
1081           rewrite <- IHΣ1 at 2.
1082           rewrite <- IHΣ2 at 2.
1083           reflexivity.
1084         idtac.
1085         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
1086         apply boost.
1087         take_simplify.
1088         simpl.
1089         replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1090         rewrite mapOptionTree_compose.
1091         rewrite mapOptionTree_compose.
1092         rewrite unlev_relev.
1093         apply ga_second.
1094       rewrite take_lemma'.
1095       reflexivity.
1096
1097     destruct case_RRight.
1098       simpl.
1099       destruct l as [|ec lev].
1100       simpl.
1101         replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1102         apply nd_rule.
1103         apply RRight.
1104         induction Σ; try destruct a; auto.
1105         simpl.
1106         rewrite <- IHΣ1.
1107         rewrite <- IHΣ2.
1108         reflexivity.
1109       repeat drop_simplify.
1110         rewrite drop_to_nothing.
1111         simpl.
1112         eapply nd_comp.
1113         Focus 2.
1114         eapply nd_rule.
1115         eapply RArrange.
1116         eapply ALeft.
1117         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1118           induction Σ; try destruct a; auto.
1119           simpl.
1120           rewrite <- IHΣ1 at 2.
1121           rewrite <- IHΣ2 at 2.
1122           reflexivity.
1123         idtac.
1124         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1125         apply boost.
1126         take_simplify.
1127         simpl.
1128         replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1129         rewrite mapOptionTree_compose.
1130         rewrite mapOptionTree_compose.
1131         rewrite unlev_relev.
1132         apply ga_first.
1133       rewrite take_lemma'.
1134       reflexivity.
1135
1136     destruct case_RVoid.
1137       simpl.
1138       destruct l.
1139       apply nd_rule.
1140       apply RVoid.
1141       drop_simplify.
1142       take_simplify.
1143       simpl.
1144       apply ga_id.
1145
1146     destruct case_RAppT.
1147       simpl. destruct lev; simpl.
1148       unfold flatten_leveled_type.
1149       simpl.
1150       rewrite flatten_commutes_with_HaskTAll.
1151       rewrite flatten_commutes_with_substT.
1152       apply nd_rule.
1153       apply RAppT.
1154       apply Δ.
1155       apply Δ.
1156       apply (Prelude_error "found type application at level >0; this is not supported").
1157
1158     destruct case_RAbsT.
1159       simpl. destruct lev; simpl.
1160       rewrite flatten_commutes_with_HaskTAll.
1161       rewrite flatten_commutes_with_HaskTApp.
1162       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1163       simpl.
1164       set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1165       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1166       assert (a=q').
1167         unfold a.
1168         unfold q'.
1169         clear a q'.
1170         induction Σ.
1171           destruct a.
1172           simpl.
1173           rewrite flatten_commutes_with_weakLT.
1174           reflexivity.
1175           reflexivity.
1176           simpl.
1177           rewrite <- IHΣ1.
1178           rewrite <- IHΣ2.
1179           reflexivity.
1180       rewrite H.
1181       apply nd_id.
1182       apply Δ.
1183       apply Δ.
1184       apply (Prelude_error "found type abstraction at level >0; this is not supported").
1185
1186     destruct case_RAppCo.
1187       simpl. destruct lev; simpl.
1188       unfold flatten_type.
1189       simpl.
1190       apply nd_rule.
1191       apply RAppCo.
1192       apply flatten_coercion.
1193       apply γ.
1194       apply (Prelude_error "found coercion application at level >0; this is not supported").
1195
1196     destruct case_RAbsCo.
1197       simpl. destruct lev; simpl.
1198       unfold flatten_type.
1199       simpl.
1200       apply (Prelude_error "AbsCo not supported (FIXME)").
1201       apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1202
1203     destruct case_RLetRec.
1204       rename t into lev.
1205       simpl. destruct lev; simpl.
1206       apply nd_rule.
1207       set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1208       replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1209       apply q.
1210         induction y; try destruct a; auto.
1211         simpl.
1212         rewrite IHy1.
1213         rewrite IHy2.
1214         reflexivity.
1215       repeat drop_simplify.
1216       repeat take_simplify.
1217       simpl.
1218       rewrite drop_to_nothing.
1219       eapply nd_comp.
1220         eapply nd_rule.
1221         eapply RArrange.
1222         eapply AComp.
1223         eapply ARight.
1224         apply arrangeCancelEmptyTree with (q:=y).
1225           induction y; try destruct a; auto.
1226           simpl.
1227           rewrite <- IHy1.
1228           rewrite <- IHy2.
1229           reflexivity.
1230         apply ACanL.
1231         rewrite take_lemma'.
1232         set (mapOptionTree (flatten_type ○ unlev) (take_lev (h :: lev) lri)) as lri'.
1233         set (mapOptionTree flatten_leveled_type (drop_lev (h :: lev) lri)) as lri''.
1234         replace (mapOptionTree (flatten_type ○ unlev) (y @@@ (h :: lev))) with (mapOptionTree flatten_type y).
1235         apply boost.
1236         apply ga_loopl.
1237         rewrite <- mapOptionTree_compose.
1238         simpl.
1239         reflexivity.
1240
1241     destruct case_RCase.
1242       destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl.
1243       apply nd_rule.
1244       rewrite <- mapOptionTree_compose.
1245       replace (mapOptionTree
1246         (fun x  => flatten_judgment (pcb_judg (snd x)))
1247         alts,, [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [flatten_type (caseType tc avars)] @ nil])
1248       with
1249         (mapOptionTree
1250            (fun x  => @pcb_judg tc Γ Δ nil (flatten_type tbranches) avars (fst x) (snd x))
1251            alts,,
1252            [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [caseType tc avars] @ nil]).
1253       replace (mapOptionTree flatten_leveled_type
1254         (mapOptionTreeAndFlatten
1255            (fun x  => (snd x)) alts))
1256       with (mapOptionTreeAndFlatten
1257            (fun x =>
1258             (snd x)) alts).
1259       apply RCase.
1260       admit.
1261       admit.
1262
1263     destruct case_SBrak.
1264       simpl.
1265       destruct lev.
1266       drop_simplify.
1267       set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1268       take_simplify.
1269       rewrite take_lemma'.
1270       simpl.
1271       rewrite mapOptionTree_compose.
1272       rewrite mapOptionTree_compose.
1273       rewrite unlev_relev.
1274       rewrite <- mapOptionTree_compose.
1275       simpl.
1276       rewrite krunk.
1277       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1278       set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1279       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1280       unfold empty_tree.
1281       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
1282       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
1283       refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1284       eapply nd_comp; [ idtac | eapply arrange_brak ].
1285       unfold succ_host.
1286       unfold succ_guest.
1287       eapply nd_rule.
1288         eapply RArrange.
1289         apply AExch.
1290       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1291
1292     destruct case_SEsc.
1293       simpl.
1294       destruct lev.
1295       simpl.
1296       unfold flatten_leveled_type at 2.
1297       simpl.
1298       rewrite krunk.
1299       rewrite mapOptionTree_compose.
1300       take_simplify.
1301       drop_simplify.
1302       simpl.
1303       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
1304       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
1305       simpl.
1306       rewrite take_lemma'.
1307       rewrite unlev_relev.
1308       rewrite <- mapOptionTree_compose.
1309       eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1310
1311       set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1312       destruct q'.
1313       destruct s.
1314       rewrite e.
1315       clear e.
1316
1317       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1318       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1319
1320       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1321       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1322       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
1323       eapply nd_comp; [ idtac | eapply RLet ].
1324       eapply nd_comp; [ apply nd_llecnac | idtac ].
1325       apply nd_prod; [ idtac | eapply boost ].
1326       induction x.
1327         apply ga_id.
1328         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
1329         simpl.
1330         apply ga_join.
1331           apply IHx1.
1332           apply IHx2.
1333           simpl.
1334           apply postcompose.
1335
1336       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1337       apply ga_cancell.
1338       apply firstify.
1339
1340       induction x.
1341         destruct a; simpl.
1342         apply ga_id.
1343         simpl.
1344         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1345         apply ga_cancell.
1346         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1347         eapply firstify.
1348         apply IHx1.
1349         apply secondify.
1350         apply IHx2.
1351
1352       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1353       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1354
1355       replace (mapOptionTree (fun ht => levels_to_tcode (unlev ht) (getlev ht) @@  nil) (drop_lev (ec :: nil) succ))
1356         with (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)).
1357       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply AExch | idtac ].
1358       apply ga_kappa.
1359       induction succ.
1360         destruct a.
1361         destruct l.
1362         Transparent drop_lev.
1363         simpl.
1364         unfold drop_lev.
1365         Opaque drop_lev.
1366         unfold mkDropFlags.
1367         simpl.
1368         destruct (General.list_eq_dec h1 (ec :: nil)).
1369         simpl.
1370         auto.
1371         simpl.
1372         unfold flatten_leveled_type.
1373         simpl.
1374         auto.
1375         simpl.
1376         auto.
1377         simpl.
1378         drop_simplify.
1379         simpl.
1380         rewrite IHsucc1.
1381         rewrite IHsucc2.
1382         reflexivity.
1383
1384       (* nesting too deep *)
1385       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1386       Defined.
1387
1388   Definition flatten_proof :
1389     forall  {h}{c},
1390       ND  Rule h c ->
1391       ND  Rule h c.
1392     apply (Prelude_error "sorry, non-skolemized flattening isn't implemented").
1393     Defined.
1394
1395   Definition skolemize_and_flatten_proof :
1396     forall  {h}{c},
1397       ND  Rule h c ->
1398       ND  Rule
1399            (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1400            (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1401     intros.
1402     rewrite mapOptionTree_compose.
1403     rewrite mapOptionTree_compose.
1404     apply flatten_skolemized_proof.
1405     apply skolemize_proof.
1406     apply X.
1407     Defined.
1408
1409
1410   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1411    * calculate it, and show that the flattening procedure above drives it down by one *)
1412
1413   (*
1414   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1415     { fmor := FlatteningFunctor_fmor }.
1416
1417   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1418     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1419
1420   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1421     refine {| plsmme_pl := PCF n Γ Δ |}.
1422     Defined.
1423
1424   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1425     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1426     Defined.
1427
1428   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1429     Defined.
1430
1431   (* 5.1.4 *)
1432   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1433     Defined.
1434   *)
1435   (*  ... and the retraction exists *)
1436
1437 End HaskFlattener.
1438
1439 Implicit Arguments garrow [ ].