X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=b46f4d22abd3ede84f4bc290ba5bc0b8073a8329;hp=b55dcf5e7c11306e921c790a4b978428b9598888;hb=2da83e6cfd727f142489859160b7d57bfa80a3be;hpb=e8d9db77f48f7710b5eec6cba6fdaf4650a48c88

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index b55dcf5..b46f4d2 100644
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -14,37 +14,24 @@ Require Import Coq.Lists.List.
 
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskCoreVars.
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.
-Require Import NaturalDeductionCategory.
-
-Require Import Algebras_ch4.
-Require Import Categories_ch1_3.
-Require Import Functors_ch1_4.
-Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
-Require Import OppositeCategories_ch1_6_2.
-Require Import Enrichment_ch2_8.
-Require Import Subcategories_ch7_1.
-Require Import NaturalTransformations_ch7_4.
-Require Import NaturalIsomorphisms_ch7_5.
-Require Import BinoidalCategories.
-Require Import PreMonoidalCategories.
-Require Import MonoidalCategories_ch7_8.
-Require Import Coherence_ch7_8.
 
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskProof.
 Require Import HaskStrongToProof.
 Require Import HaskProofToStrong.
-Require Import ProgrammingLanguage.
-Require Import HaskProgrammingLanguage.
-Require Import PCF.
+Require Import HaskWeakToStrong.
 
 Open Scope nd_scope.
+Set Printing Width 130.
 
 (*
  *  The flattening transformation.  Currently only TWO-level languages are
@@ -56,19 +43,49 @@ Open Scope nd_scope.
  *)
 Section HaskFlattener.
 
-  (* this actually has nothing to do with categories; it shows that proofs [|-A]//[|-B] are one-to-one with []//[A|-B] *)
-  (* TODO Lemma hom_functor_full*)
-
-  (* lemma: if a proof from no hypotheses contains no Brak's or Esc's, then the context contains no variables at level!=0 *)
+  Definition arrange :
+    forall {T} (Σ:Tree ??T) (f:T -> bool),
+      Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
+    intros.
+    induction Σ.
+      simpl.
+      destruct a.
+      simpl.
+      destruct (f t); simpl.
+      apply RuCanL.
+      apply RuCanR.
+      simpl.
+      apply RuCanL.
+      simpl in *.
+      eapply RComp; [ idtac | apply arrangeSwapMiddle ].
+      eapply RComp.
+      eapply RLeft.
+      apply IHΣ2.
+      eapply RRight.
+      apply IHΣ1.
+      Defined.
 
-  Definition minus' n m :=
-    match m with
-      | 0 => n
-      | _ => match n with
-               | 0 => 0
-               | _ => n - m
-             end
-    end.
+  Definition arrange' :
+    forall {T} (Σ:Tree ??T) (f:T -> bool),
+      Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
+    intros.
+    induction Σ.
+      simpl.
+      destruct a.
+      simpl.
+      destruct (f t); simpl.
+      apply RCanL.
+      apply RCanR.
+      simpl.
+      apply RCanL.
+      simpl in *.
+      eapply RComp; [ apply arrangeSwapMiddle | idtac ].
+      eapply RComp.
+      eapply RLeft.
+      apply IHΣ2.
+      eapply RRight.
+      apply IHΣ1.
+      Defined.
 
   Ltac eqd_dec_refl' :=
     match goal with
@@ -77,44 +94,146 @@ Section HaskFlattener.
           [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
   end.
 
-  (* The opposite: replace any type which is NOT at level "lev" with None *)
-  Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
-    mapTree (fun t => match t with
-                        | Some (ttype @@ tlev) => if eqd_dec tlev lev then Some ttype else None
-                        | _                    => None
-                      end) tt.
+  Context (hetmet_flatten : WeakExprVar).
+  Context (hetmet_unflatten : WeakExprVar).
+  Context (hetmet_id      : WeakExprVar).
+  Context {unitTy : forall TV, RawHaskType TV ★                                          }.
+  Context {prodTy : forall TV, RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
+  Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
+
+  Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
+    fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr).
+
+  Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
+    fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite).
+
+  Class garrow :=
+  { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec a a @@ l] ]
+  ; ga_cancelr   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
+  ; ga_cancell   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
+  ; ga_uncancelr : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
+  ; ga_uncancell : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
+  ; ga_assoc     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
+  ; ga_unassoc   : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
+  ; ga_swap      : ∀ Γ Δ ec l a b  , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
+  ; ga_drop      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec a [] @@ l] ]
+  ; ga_copy      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
+  ; ga_first     : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >          [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
+  ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >          [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
+  ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
+  ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
+  ; 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] ] 
+  ; ga_apply     : ∀ Γ Δ ec l a a' b c, ND Rule []
+                                  [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
+  ; ga_kappa     : ∀ Γ Δ ec l a b Σ, ND Rule
+  [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
+  [Γ > Δ > Σ          |- [@ga_mk Γ ec a  b @@ l] ]
+  }.
+  Context `(gar:garrow).
+
+  Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
+
+  (*
+   *  The story:
+   *    - code types <[t]>@c                                                become garrows  c () t 
+   *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
+   *    - free variables at the level of the succedent become 
+   *)
+  Fixpoint garrowfy_raw_codetypes {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
+    match exp with
+    | TVar    _  x          => TVar x
+    | TAll     _ y          => TAll   _  (fun v => garrowfy_raw_codetypes (y v))
+    | TApp   _ _ x y        => TApp      (garrowfy_raw_codetypes x) (garrowfy_raw_codetypes y)
+    | TCon       tc         => TCon      tc
+    | TCoerc _ t1 t2 t      => TCoerc    (garrowfy_raw_codetypes t1) (garrowfy_raw_codetypes t2)
+                                         (garrowfy_raw_codetypes t)
+    | TArrow                => TArrow
+    | TCode      v e        => gaTy TV v (unitTy TV) (garrowfy_raw_codetypes e)
+    | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (garrowfy_raw_codetypes_list _ lt)
+    end
+    with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
+    match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
+    | TyFunApp_nil               => TyFunApp_nil
+    | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes t) (garrowfy_raw_codetypes_list _ rest)
+    end.
+  Definition garrowfy_code_types {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
+    fun TV ite =>
+      garrowfy_raw_codetypes (ht TV ite).
+
+  Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) := fun TV ite => TVar (ec TV ite).
+
+  Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
+    match lev with
+      | nil      => garrowfy_code_types ht
+      | ec::lev' => @ga_mk _ (v2t ec) [] [garrowfy_leveled_code_types' ht lev']
+    end.
+
+  Definition garrowfy_leveled_code_types {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
+    match ht with
+      htt @@ lev =>
+      garrowfy_leveled_code_types' htt lev @@ nil
+    end.
+
+  Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
+    fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
 
   (* In a tree of types, replace any type at depth "lev" or greater None *)
-  Definition drop_depth {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
-    mapTree (fun t => match t with
-                        | Some (ttype @@ tlev) => if eqd_dec tlev lev then None else t
-                        | _ => t
-                      end) tt.
+  Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
+    mkFlags (liftBoolFunc false (levelMatch lev)) tt.
 
-  Lemma drop_depth_lemma : forall Γ (lev:HaskLevel Γ) x, drop_depth lev [x @@  lev] = [].
+  Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
+    dropT (mkDropFlags lev tt).
+
+  (* The opposite: replace any type which is NOT at level "lev" with None *)
+  Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
+    mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
+
+  Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
+    mapOptionTree (fun x => garrowfy_code_types (unlev x)) (dropT (mkTakeFlags lev tt)).
+(*
+    mapOptionTree (fun x => garrowfy_code_types (unlev x))
+    (maybeTree (takeT tt (mkFlags (
+      fun t => match t with
+                 | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
+                 | _                    => true
+               end
+    ) tt))).
+
+  Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
+    match t with
+      | None   => []
+      | Some x => x
+    end.
+*)
+
+  Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@  lev] = [].
     intros; simpl.
     Opaque eqd_dec.
-    unfold drop_depth.
+    unfold drop_lev.
+    simpl.
+    unfold mkDropFlags.
     simpl.
     Transparent eqd_dec.
     eqd_dec_refl'.
     auto.
     Qed.
 
-  Lemma drop_depth_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_depth (ec::lev) [x @@  (ec :: lev)] = [].
+  Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@  (ec :: lev)] = [].
     intros; simpl.
     Opaque eqd_dec.
-    unfold drop_depth.
+    unfold drop_lev.
+    unfold mkDropFlags.
     simpl.
     Transparent eqd_dec.
     eqd_dec_refl'.
     auto.
     Qed.
 
-  Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@  lev] = [x].
+  Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@  lev] = [garrowfy_code_types x].
     intros; simpl.
     Opaque eqd_dec.
     unfold take_lev.
+    unfold mkTakeFlags.
     simpl.
     Transparent eqd_dec.
     eqd_dec_refl'.
@@ -123,14 +242,14 @@ Section HaskFlattener.
 
   Ltac drop_simplify :=
     match goal with
-      | [ |- context[@drop_depth ?G ?L [ ?X @@ ?L ] ] ] =>
-        rewrite (drop_depth_lemma G L X)
-      | [ |- context[@drop_depth ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
-        rewrite (drop_depth_lemma_s G L E X)
-      | [ |- context[@drop_depth ?G ?N (?A,,?B)] ] =>
-      change (@drop_depth G N (A,,B)) with ((@drop_depth G N A),,(@drop_depth G N B))
-      | [ |- context[@drop_depth ?G ?N (T_Leaf None)] ] =>
-      change (@drop_depth G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
+      | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
+        rewrite (drop_lev_lemma G L X)
+      | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
+        rewrite (drop_lev_lemma_s G L E X)
+      | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
+      change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
+      | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
+      change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
     end.
 
   Ltac take_simplify :=
@@ -143,90 +262,32 @@ Section HaskFlattener.
       change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
     end.
 
-  Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
-    match tt with
-      | T_Leaf None     => unit
-      | T_Leaf (Some x) => x
-      | T_Branch b1 b2  => merge (reduceTree unit merge b1) (reduceTree unit merge b2)
-    end.
-
-  Set Printing Width 130.
+  (* AXIOMS *)
 
-  Context {unitTy : forall TV, RawHaskType TV  ★             }.
-  Context {prodTy : forall TV, RawHaskType TV (★ ⇛ ★ ⇛ ★)    }.
-  Context {gaTy   : forall TV, RawHaskType TV (★ ⇛ ★ ⇛ ★ ⇛ ★)}.
+  Axiom literal_types_unchanged : forall Γ l, garrowfy_code_types (literalType l) = literalType(Γ:=Γ) l.
 
-  Definition ga_tree      := fun TV tr => reduceTree (unitTy TV) (fun t1 t2 => TApp (TApp (prodTy TV) t1) t2) tr.
-  Definition ga'          := fun TV ec ant' suc' => TApp (TApp (TApp (gaTy TV) ec) (ga_tree TV ant')) (ga_tree TV suc').
-  Definition ga {Γ} : HaskType Γ ★ -> Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> HaskType Γ ★ :=
-    fun ec ant suc =>
-                               fun TV ite =>
-                                 let ant' := mapOptionTree (fun x => x TV ite) ant in
-                                   let suc' := mapOptionTree (fun x => x TV ite) suc in
-                                     ga' TV (ec TV ite) ant' suc'.
+  Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
+    HaskCoercion Γ Δ (garrowfy_code_types σ ∼∼∼ garrowfy_code_types τ).
 
-  Class garrow :=
-  { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec a a @@ l] ]
-  ; ga_cancelr   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec (a,,[]) a @@ l] ]
-  ; ga_cancell   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec ([],,a) a @@ l] ]
-  ; ga_uncancelr : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec a (a,,[]) @@ l] ]
-  ; ga_uncancell : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec a ([],,a) @@ l] ]
-  ; ga_assoc     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
-  ; ga_unassoc   : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
-  ; ga_swap      : ∀ Γ Δ ec l a b  , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec (a,,b) (b,,a) @@ l] ]
-  ; ga_drop      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec a [] @@ l] ]
-  ; ga_copy      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec a (a,,a) @@ l] ]
-  ; ga_first     : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >          [@ga Γ ec a b @@ l] |- [@ga Γ ec (a,,x) (b,,x) @@ l] ]
-  ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >          [@ga Γ ec a b @@ l] |- [@ga Γ ec (x,,a) (x,,b) @@ l] ]
-  ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec [] [literalType lit] @@ l] ]
-  ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga Γ ec (a,,[b]) [c] @@ l] |- [@ga Γ ec a [b ---> c] @@ l] ]
-  ; ga_comp      : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ l],,[@ga Γ ec b c @@ l] |- [@ga Γ ec a c @@ l] ] 
-  ; ga_apply     : ∀ Γ Δ ec l a a' b c, ND Rule []
-                                  [Γ > Δ > [@ga Γ ec a [b ---> c] @@ l],,[@ga Γ ec a' [b] @@ l] |- [@ga Γ ec (a,,a') [c] @@ l] ]
-  ; ga_kappa     : ∀ Γ Δ ec l a b Σ, ND Rule
-  [Γ > Δ > Σ,,[@ga Γ ec [] a @@ l] |- [@ga Γ ec [] b @@ l] ]
-  [Γ > Δ > Σ          |- [@ga Γ ec a  b @@ l] ]
-  }.
-  Context `(gar:garrow).
+  Axiom garrowfy_commutes_with_substT :
+    forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
+    garrowfy_code_types  (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes  (σ TV ite v))
+      (garrowfy_code_types  τ).
 
-  Notation "a ~~~~> b" := (@ga _ _ a b) (at level 20).
+  Axiom garrowfy_commutes_with_HaskTAll :
+    forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
+    garrowfy_code_types  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)).
 
-  (*
-   *  The story:
-   *    - code types <[t]>@c                                                become garrows  c () t 
-   *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
-   *    - free variables at the level of the succedent become 
-   *)
-  Fixpoint garrowfy_raw_codetypes {TV}{κ}(depth:nat)(exp: RawHaskType TV κ) : RawHaskType TV κ :=
-    match exp with
-    | TVar    _  x        => TVar x
-    | TAll     _ y        => TAll   _  (fun v => garrowfy_raw_codetypes depth (y v))
-    | TApp   _ _ x y      => TApp      (garrowfy_raw_codetypes depth x) (garrowfy_raw_codetypes depth y)
-    | TCon       tc       => TCon      tc
-    | TCoerc _ t1 t2 t    => TCoerc    (garrowfy_raw_codetypes depth t1) (garrowfy_raw_codetypes depth t2)
-                                       (garrowfy_raw_codetypes depth t)
-    | TArrow              => TArrow
-    | TCode      v e      => match depth with
-                               | O          => ga' TV v [] [(*garrowfy_raw_codetypes depth*) e]
-                               | (S depth') => TCode v (garrowfy_raw_codetypes depth' e)
-                             end
-    | TyFunApp     tfc lt => TyFunApp tfc (garrowfy_raw_codetypes_list _ depth lt)
-    end
-    with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(depth:nat)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
-    match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
-    | TyFunApp_nil               => TyFunApp_nil
-    | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes depth t) (garrowfy_raw_codetypes_list _ depth rest)
-    end.
-  Definition garrowfy_code_types {Γ}{κ}(n:nat)(ht:HaskType Γ κ) : HaskType Γ κ :=
-    fun TV ite =>
-      garrowfy_raw_codetypes n (ht TV ite).
-  Definition garrowfy_leveled_code_types {Γ}(n:nat)(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
-    match ht with htt @@ htlev => garrowfy_code_types (minus' n (length htlev)) htt @@ htlev end.
+  Axiom garrowfy_commutes_with_HaskTApp :
+    forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
+    garrowfy_code_types  (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
+    HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes  (σ TV ite v))) (FreshHaskTyVar κ).
 
-  Axiom literal_types_unchanged : forall n Γ l, garrowfy_code_types n (literalType l) = literalType(Γ:=Γ) l.
+  Axiom garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ  t,
+    garrowfy_leveled_code_types  (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types  t).
 
-  Axiom flatten_coercion : forall n Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
-    HaskCoercion Γ Δ (garrowfy_code_types n σ ∼∼∼ garrowfy_code_types n τ).
+  Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
+    garrowfy_code_types (g v) = g v.
 
   (* This tries to assign a single level to the entire succedent of a judgment.  If the succedent has types from different
    * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
@@ -245,58 +306,129 @@ Section HaskFlattener.
         end
     end.
 
-  Definition v2t {Γ}(ec:HaskTyVar Γ ★) := fun TV ite => TVar (ec TV ite).
+  Definition unlev' {Γ} (x:LeveledHaskType Γ ★) :=
+    garrowfy_code_types (unlev x).
 
   (* "n" is the maximum depth remaining AFTER flattening *)
-  Definition flatten_judgment (n:nat)(j:Judg) :=
+  Definition flatten_judgment (j:Judg) :=
     match j as J return Judg with
       Γ > Δ > ant |- suc =>
-        match (match getjlev suc with
-                 | nil        => inl _ tt
-                 | (ec::lev') => if eqd_dec (length lev') n
-                                 (* If the judgment's level is the deepest in the proof, flatten it by turning
-                                  * all antecedent variables at this level into None's, garrowfying any other
-                                  * antecedent variables (from other levels) at the same depth, and turning the
-                                  * succedent into a garrow type *)
-                                 then inr _ (Γ > Δ > mapOptionTree (garrowfy_leveled_code_types n) (drop_depth (ec::lev') ant)
-                                                  |- [ga (v2t ec) (take_lev (ec::lev') ant) (mapOptionTree unlev suc) @@ lev'])
-                                 else inl _ tt
-               end) with
-
-        (* otherwise, just garrowfy all code types of the specified depth, throughout the judgment *)
-        | inl tt => Γ > Δ > mapOptionTree (garrowfy_leveled_code_types n) ant |- mapOptionTree (garrowfy_leveled_code_types n) suc
-        | inr r => r
+        match getjlev suc with
+          | nil        => Γ > Δ > mapOptionTree garrowfy_leveled_code_types ant
+                               |- mapOptionTree garrowfy_leveled_code_types suc
+
+          | (ec::lev') => Γ > Δ > mapOptionTree garrowfy_leveled_code_types (drop_lev (ec::lev') ant)
+                               |- [ga_mk (v2t ec)
+                                         (take_lev (ec::lev') ant)
+                                         (mapOptionTree unlev' suc)  (* we know the level of all of suc *)
+                                         @@ nil]
         end
     end.
 
-  Definition boost : forall Γ Δ ant x y,
-     ND Rule []                   [ Γ > Δ > x   |- y ] ->
-     ND Rule [ Γ > Δ > ant |- x ] [ Γ > Δ > ant |- y ].
-     admit.
+  Definition boost : forall Γ Δ ant x y {lev},
+    ND Rule []                          [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
+    ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant      |- [y@@lev] ].
+    intros.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
+    apply nd_prod.
+    apply nd_id.
+    eapply nd_comp.
+      apply X.
+      eapply nd_rule.
+      eapply RArrange.
+      apply RuCanL.
+      Defined.
+
+  Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
+     ND Rule [] [ Γ > Δ > Σ                        |- [@ga_mk Γ ec a b @@ lev] ] ->
+     ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
+     intros.
+     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+     eapply nd_comp; [ idtac
+       | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
+     eapply nd_comp; [ apply nd_llecnac | idtac ].
+     apply nd_prod.
+     apply X.
+     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+     apply ga_comp.
      Defined.
 
-  Definition postcompose : ∀ Γ Δ ec lev a b c,
-     ND Rule [] [ Γ > Δ > []                    |- [@ga Γ ec a b @@ lev] ] ->
-     ND Rule [] [ Γ > Δ > [@ga Γ ec b c @@ lev] |- [@ga Γ ec a c @@ lev] ].
-     admit.
+  Definition precompose Γ Δ ec : forall a x y z lev,
+    ND Rule
+      [ Γ > Δ > a                           |- [@ga_mk _ ec y z @@ lev] ]
+      [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
+    intros.
+    eapply nd_comp.
+    apply nd_rlecnac.
+    eapply nd_comp.
+    eapply nd_prod.
+    apply nd_id.
+    eapply ga_comp.
+
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+
+    apply nd_rule.
+    apply RLet.
+    Defined.
+
+  Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
+     ND Rule [] [ Γ > Δ > Σ                           |- [@ga_mk Γ ec b c @@ lev] ] ->
+     ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
+     intros.
+     eapply nd_comp.
+     apply X.
+     apply precompose.
      Defined.
 
-  Definition seq : ∀ Γ Δ lev a b,
-     ND Rule [] [ Γ > Δ > [] |- [a @@ lev] ] ->
-     ND Rule [] [ Γ > Δ > [] |- [b @@ lev] ] ->
-     ND Rule [] [ Γ > Δ > [] |- [a @@ lev],,[b @@ lev] ].
-     admit.
+  Definition postcompose : ∀ Γ Δ ec lev a b c,
+     ND Rule [] [ Γ > Δ > []                    |- [@ga_mk Γ ec a b @@ lev] ] ->
+     ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
+     intros.
+     eapply nd_comp.
+     apply postcompose'.
+     apply X.
+     apply nd_rule.
+     apply RArrange.
+     apply RCanL.
      Defined.
 
+  Definition firstify : ∀ Γ Δ ec lev a b c Σ,
+    ND Rule [] [ Γ > Δ > Σ                     |- [@ga_mk Γ ec a b @@ lev] ] ->
+    ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
+    intros.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+    eapply nd_comp; [ apply nd_llecnac | idtac ].
+    apply nd_prod.
+    apply X.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
+    apply ga_first.
+    Defined.
+
+  Definition secondify : ∀ Γ Δ ec lev a b c Σ,
+     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b @@ lev] ] ->
+     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
+    intros.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+    eapply nd_comp; [ apply nd_llecnac | idtac ].
+    apply nd_prod.
+    apply X.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
+    apply ga_second.
+    Defined.
+
   Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ,
     ND Rule
-    [Γ > Δ > Σ |- [@ga Γ ec a  b @@ l] ] 
-    [Γ > Δ > Σ,,[@ga Γ ec [] a @@ l] |- [@ga Γ ec [] b @@ l] ].
+    [Γ > Δ > Σ |- [@ga_mk Γ ec a  b @@ l] ] 
+    [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
     intros.
     set (ga_comp Γ Δ ec l [] a b) as q.
 
     set (@RLet Γ Δ) as q'.
-    set (@RLet Γ Δ [@ga _ ec [] a @@ l] Σ (@ga _ ec [] b) (@ga _ ec a b) l) as q''.
+    set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
     eapply nd_comp.
     Focus 2.
     eapply nd_rule.
@@ -317,21 +449,22 @@ Section HaskFlattener.
     apply q.
     Defined.
 
-(*
+  (* useful for cutting down on the pretty-printed noise
+  
   Notation "`  x" := (take_lev _ x) (at level 20).
   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
-  Notation "``` x" := (drop_depth _ x) (at level 20).
-*)
+  Notation "``` x" := (drop_lev _ x) (at level 20).
+  *)
   Definition garrowfy_arrangement' :
     forall Γ (Δ:CoercionEnv Γ)
-      (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
-      ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev] ].
+      (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
+      ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
 
       intros Γ Δ ec lev.
       refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
-           ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev]] :=
+           ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil]] :=
         match r as R in Arrange A B return
-          ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ lev]]
+          ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ nil]]
           with
           | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
           | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
@@ -340,36 +473,49 @@ Section HaskFlattener.
           | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
           | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
           | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
-          | RWeak  a             => let case_RWeak := tt  in ga_drop  _ _ _ _ _ 
+          | RWeak  a             => let case_RWeak := tt  in ga_drop _ _ _ _ _ 
           | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _ 
           | RLeft  a b c r'      => let case_RLeft := tt  in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
           | RRight a b c r'      => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
-          | RComp  a b c r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
+          | RComp  c b a r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
         end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
 
         destruct case_RComp.
-          refine ( _ ;; boost _ _ _ _ _ (ga_comp _ _ _ _ _ _ _)).
-          apply seq.
+          set (take_lev (ec :: lev) a) as a' in *.
+          set (take_lev (ec :: lev) b) as b' in *.
+          set (take_lev (ec :: lev) c) as c' in *.
+          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+          eapply nd_comp; [ idtac | eapply nd_rule; apply
+             (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
+          eapply nd_comp; [ apply nd_llecnac | idtac ].
+          apply nd_prod.
           apply r2'.
+          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
+          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
+          eapply nd_comp; [ idtac | eapply nd_rule;  apply 
+            (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
+          eapply nd_comp; [ apply nd_llecnac | idtac ].
+          eapply nd_prod.
           apply r1'.
+          apply ga_comp.
           Defined.
 
   Definition garrowfy_arrangement :
     forall Γ (Δ:CoercionEnv Γ) n
-      (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
+      (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
       ND Rule
-      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth n ant1)
-        |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree unlev succ) @@ lev]]
-      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth n ant2)
-        |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree unlev succ) @@ lev]].
+      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
+        |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
+      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant2)
+        |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree (unlev' ) succ) @@ nil]].
       intros.
       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
       apply nd_rule.
       apply RArrange.
       refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
         match r as R in Arrange A B return
-          Arrange (mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth _ A))
-          (mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth _ B)) with
+          Arrange (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ A))
+          (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ B)) with
           | RCanL  a             => let case_RCanL := tt  in RCanL _
           | RCanR  a             => let case_RCanR := tt  in RCanR _
           | RuCanL a             => let case_RuCanL := tt in RuCanL _
@@ -386,9 +532,9 @@ Section HaskFlattener.
         Defined.
 
   Definition flatten_arrangement :
-    forall n Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
-      ND Rule (mapOptionTree (flatten_judgment n) [Γ > Δ > ant1 |- succ])
-      (mapOptionTree (flatten_judgment n) [Γ > Δ > ant2 |- succ]).
+    forall  Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
+      ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
+      (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
     intros.
     simpl.
     set (getjlev succ) as succ_lev.
@@ -412,49 +558,128 @@ Section HaskFlattener.
         apply RRight; auto.
         eapply RComp; [ apply IHr1 | apply IHr2 ].
 
-    set (Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n) as lev_is_n.
-      assert (lev_is_n=Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n).
-        reflexivity.
-      destruct lev_is_n.
-        rewrite <- e.
-        apply garrowfy_arrangement.
+      apply garrowfy_arrangement.
         apply r.
-        auto.
-      apply nd_rule.
-      apply RArrange.
-      induction r; simpl.
-        apply RCanL.
-        apply RCanR.
-        apply RuCanL.
-        apply RuCanR.
-        apply RAssoc.
-        apply RCossa.
-        apply RExch.
-        apply RWeak.
-        apply RCont.
-        apply RLeft; auto.
-        apply RRight; auto.
-        eapply RComp; [ apply IHr1 | apply IHr2 ].
         Defined.
 
+  Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
+    ND Rule [] [Γ > Δ > Σ₁     |- [@ga_mk _ ec [] a      @@ nil]] ->
+    ND Rule [] [Γ > Δ > Σ₂     |- [@ga_mk _ ec [] b      @@ nil]] ->
+    ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
+    intro pfa.
+    intro pfb.
+    apply secondify with (c:=a)  in pfb.
+    eapply nd_comp.
+    Focus 2.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ eapply nd_llecnac | idtac ].
+    eapply nd_prod.
+    apply pfb.
+    clear pfb.
+    apply postcompose'.
+    eapply nd_comp.
+    apply pfa.
+    clear pfa.
+    apply boost.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+    apply precompose'.
+    apply ga_uncancelr.
+    apply nd_id.
+    Defined.
+
   Definition arrange_brak : forall Γ Δ ec succ t,
-    ND Rule
-     [Γ > Δ >
-      mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec :: nil) succ),,
-      [(@ga _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@  nil] |- 
-      [(@ga _ (v2t ec) [] [t]) @@  nil]]
-        [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types 0) succ |- [(@ga _ (v2t ec) [] [t]) @@  nil]].
-    admit.
+   ND Rule
+     [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
+      [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@  nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]]
+     [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]].
+    intros.
+    unfold drop_lev.
+    set (@arrange' _ succ (levelMatch (ec::nil))) as q.
+    set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
+    eapply nd_comp.
+    Focus 2.
+    eapply nd_rule.
+    eapply RArrange.
+    apply y.
+    idtac.
+    clear y q.
+    simpl.
+    eapply nd_comp; [ apply nd_llecnac | idtac ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    apply nd_prod.
+    Focus 2.
+    apply nd_id.
+    idtac.
+    induction succ; try destruct a; simpl.
+    unfold take_lev.
+    unfold mkTakeFlags.
+    unfold mkFlags.
+    unfold bnot.
+    simpl.
+    destruct l as [t' lev'].
+    destruct lev' as [|ec' lev'].
+    simpl.
+    apply ga_id.
+    unfold levelMatch.
+    set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
+    destruct q.
+    inversion e; subst.
+    simpl.
+    apply nd_rule.
+    apply RVar.
+    simpl.
+    apply ga_id.
+    apply ga_id.
+    unfold take_lev.
+    simpl.
+    apply ga_join.
+      apply IHsucc1.
+      apply IHsucc2.
     Defined.
 
   Definition arrange_esc : forall Γ Δ ec succ t,
-    ND Rule
-     [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types 0) succ |- [(@ga _ (v2t ec) [] [t]) @@  nil]]
-     [Γ > Δ >
-      mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec :: nil) succ),,
-      [(@ga _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@  nil] |- [(@ga _ (v2t ec) [] [t]) @@  nil]].
-    admit.
-    Defined.
+   ND Rule
+     [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]]
+     [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
+      [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@  nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]].
+    intros.
+    unfold drop_lev.
+    set (@arrange _ succ (levelMatch (ec::nil))) as q.
+    set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
+    eapply nd_comp.
+    eapply nd_rule.
+    eapply RArrange.
+    apply y.
+    idtac.
+    clear y q.
+
+    induction succ.
+    destruct a.
+      destruct l.
+      simpl.
+      unfold mkDropFlags; simpl.
+      unfold take_lev.
+      unfold mkTakeFlags.
+      simpl.
+      destruct (General.list_eq_dec h0 (ec :: nil)).
+        simpl.
+        unfold garrowfy_leveled_code_types'.
+        rewrite e.
+        apply nd_id.
+        simpl.
+        apply nd_rule.
+        apply RArrange.
+        apply RLeft.
+        apply RWeak.
+      simpl.
+        apply nd_rule.
+        unfold take_lev.
+        simpl.
+        apply RArrange.
+        apply RLeft.
+        apply RWeak.
+      apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
+      Defined.
 
   Lemma mapOptionTree_distributes
     : forall T R (a b:Tree ??T) (f:T->R),
@@ -462,35 +687,36 @@ Section HaskFlattener.
     reflexivity.
     Qed.
 
-  Lemma garrowfy_commutes_with_substT :
-    forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
-    garrowfy_code_types n (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v))
-      (garrowfy_code_types n τ).
-    admit.
-    Qed.
-
-  Lemma garrowfy_commutes_with_HaskTAll :
-    forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
-    garrowfy_code_types n (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v)).
-    admit.
-    Qed.
-
-  Lemma garrowfy_commutes_with_HaskTApp :
-    forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
-    garrowfy_code_types n (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
-    HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v))) (FreshHaskTyVar κ).
-    admit.
-    Qed.
-
-  Lemma garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ n t,
-    garrowfy_leveled_code_types n (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types n t).
-    admit.
-    Qed.
+  Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
+    sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
+    intro T.
+    refine (fix foo t :=
+      match t with
+        | T_Leaf x => _
+        | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
+      end).
+    intros.
+    destruct x.
+    right; apply tt.
+    left.
+      exists (T_Leaf tt).
+      auto.
+    destruct b1'.
+    destruct b2'.
+    destruct s.
+    destruct s0.
+    subst.
+    left.
+    exists (x,,x0).
+    reflexivity.
+    right; auto.
+    right; auto.
+    Defined.
 
   Definition flatten_proof :
-    forall n {h}{c},
+    forall  {h}{c},
       ND Rule h c ->
-      ND Rule (mapOptionTree (flatten_judgment n) h) (mapOptionTree (flatten_judgment n) c).
+      ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
     intros.
     eapply nd_map'; [ idtac | apply X ].
     clear h c X.
@@ -520,45 +746,54 @@ Section HaskFlattener.
       end); clear X h c.
 
     destruct case_RArrange.
-      apply (flatten_arrangement n Γ Δ a b x d).
+      apply (flatten_arrangement  Γ Δ a b x d).
 
     destruct case_RBrak.
       simpl.
-      destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
       destruct lev.
-      simpl.
-      simpl.
-      destruct n.
-      change ([garrowfy_code_types 0 (<[ ec |- t ]>) @@  nil])
-        with ([ga (v2t ec) [] [t] @@  nil]).
-      refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) [t]
-        (mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec::nil) succ)) ;; _).
+      change ([garrowfy_code_types  (<[ ec |- t ]>) @@  nil])
+        with ([ga_mk (v2t ec) [] [garrowfy_code_types  t] @@  nil]).
+      refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _
+        (mapOptionTree (garrowfy_leveled_code_types) (drop_lev (ec::nil) succ)) ;; _ ).
       apply arrange_brak.
-      inversion e.
-      apply (Prelude_error "found Brak at depth >0").
-      apply (Prelude_error "found Brak at depth >0").
+      apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
 
     destruct case_REsc.
       simpl.
-      destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
       destruct lev.
       simpl.
-      destruct n.
-      change ([garrowfy_code_types 0 (<[ ec |- t ]>) @@  nil])
-        with ([ga (v2t ec) [] [t] @@  nil]).
-      refine (_ ;; ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) [t]
-        (mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec::nil) succ))).
-      apply arrange_esc.
-      inversion e.
-      apply (Prelude_error "found Esc at depth >0").
-      apply (Prelude_error "found Esc at depth >0").
+      change ([garrowfy_code_types (<[ ec |- t ]>) @@  nil])
+        with ([ga_mk (v2t ec) [] [garrowfy_code_types  t] @@  nil]).
+      eapply nd_comp; [ apply arrange_esc | idtac ].
+      set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
+      destruct q'.
+      destruct s.
+      rewrite e.
+      clear e.
+
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+      eapply nd_comp; [ apply nd_llecnac | idtac ].
+      apply nd_prod; [ idtac | eapply boost ].
+      induction x.
+      apply ga_id.
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+      apply ga_join.
+      apply IHx1.
+      apply IHx2.
+      unfold unlev'.
+      simpl.
+      apply postcompose.
+      apply ga_drop.
+
+      (* environment has non-empty leaves *)
+      apply (ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _ _).
+      apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
       
     destruct case_RNote.
       simpl.
       destruct l; simpl.
         apply nd_rule; apply RNote; auto.
-        destruct (Peano_dec.eq_nat_dec (Datatypes.length l) n).
-        apply nd_rule; apply RNote; auto.
         apply nd_rule; apply RNote; auto.
 
     destruct case_RLit.
@@ -566,13 +801,12 @@ Section HaskFlattener.
       destruct l0; simpl.
         rewrite literal_types_unchanged.
           apply nd_rule; apply RLit.
-        destruct (Peano_dec.eq_nat_dec (Datatypes.length l0) n); unfold mapTree; unfold mapOptionTree; simpl.
         unfold take_lev; simpl.
-        unfold drop_depth; simpl.
-        apply ga_lit.
+        unfold drop_lev; simpl.
+        unfold unlev'.
+        simpl.
         rewrite literal_types_unchanged.
-        apply nd_rule.
-        apply RLit.
+        apply ga_lit.
 
     destruct case_RVar.
       Opaque flatten_judgment.
@@ -583,30 +817,40 @@ Section HaskFlattener.
       unfold getjlev.
       destruct lev.
       apply nd_rule. apply RVar.
-      destruct (eqd_dec (Datatypes.length lev) n).
-
       repeat drop_simplify.      
+      unfold unlev'.
       repeat take_simplify.
       simpl.
       apply ga_id.      
 
-      apply nd_rule.
-      apply RVar.
-
     destruct case_RGlobal.
       simpl.
-      destruct l as [|ec lev]; simpl; [ apply nd_rule; apply RGlobal; auto | idtac ].
-      destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RGlobal; auto ]; simpl.
-      apply (Prelude_error "found RGlobal at depth >0").
+      rename l into g.
+      rename σ into l.
+      destruct l as [|ec lev]; simpl. 
+        destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
+          set (garrowfy_code_types (g wev)) as t.
+          set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
+          simpl in q.
+          apply nd_rule.
+          apply q.
+          apply INil.
+        destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
+          set (garrowfy_code_types (g wev)) as t.
+          set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
+          simpl in q.
+          apply nd_rule.
+          apply q.
+          apply INil.
+        apply nd_rule; rewrite globals_do_not_have_code_types.
+          apply RGlobal.
+      apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
 
     destruct case_RLam.
-      Opaque drop_depth.
+      Opaque drop_lev.
       Opaque take_lev.
       simpl.
       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
-      destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLam; auto ]; simpl.
-      rewrite <- e.
-      clear e n.
       repeat drop_simplify.
       repeat take_simplify.
       eapply nd_comp.
@@ -616,113 +860,69 @@ Section HaskFlattener.
         apply RCanR.
       apply boost.
       apply ga_curry.
-        
+
     destruct case_RCast.
       simpl.
       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
       apply flatten_coercion; auto.
-      destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RCast; auto ]; simpl.
-      apply (Prelude_error "RCast at level >0").
-      apply flatten_coercion; auto.
+      apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 
     destruct case_RJoin.
       simpl.
-      destruct (getjlev x); destruct (getjlev q).
-      apply nd_rule.
-      apply RJoin.
-      apply (Prelude_error "RJoin at depth >0").
-      apply (Prelude_error "RJoin at depth >0").
-      apply (Prelude_error "RJoin at depth >0").
+      destruct (getjlev x); destruct (getjlev q);
+        [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
+        apply (Prelude_error "RJoin at depth >0").
 
     destruct case_RApp.
       simpl.
 
       destruct lev as [|ec lev]. simpl. apply nd_rule.
-        replace (garrowfy_code_types n (tx ---> te)) with ((garrowfy_code_types n tx) ---> (garrowfy_code_types n te)).
+        replace (garrowfy_code_types  (tx ---> te)) with ((garrowfy_code_types  tx) ---> (garrowfy_code_types  te)).
         apply RApp.
-        unfold garrowfy_code_types.
-        simpl.
         reflexivity.
 
-        destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
-          eapply nd_comp.
-          eapply nd_rule.
-          apply RJoin.
-          repeat drop_simplify.
+        repeat drop_simplify.
           repeat take_simplify.
-          apply boost.
-          apply ga_apply.
-
-          replace (garrowfy_code_types (minus' n (length (ec::lev))) (tx ---> te))
-            with ((garrowfy_code_types (minus' n (length (ec::lev))) tx) --->
-              (garrowfy_code_types (minus' n (length (ec::lev))) te)).
-          apply nd_rule.
-          apply RApp.
-          unfold garrowfy_code_types.
-          simpl.
+          rewrite mapOptionTree_distributes.
+          set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
+          set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
+          set (take_lev (ec :: lev) Σ₁) as Σ₁''.
+          set (take_lev (ec :: lev) Σ₂) as Σ₂''.
+          replace (garrowfy_code_types  (tx ---> te)) with ((garrowfy_code_types  tx) ---> (garrowfy_code_types  te)).
+          apply (Prelude_error "FIXME: ga_apply").
           reflexivity.
+
 (*
-  Notation "`  x" := (take_lev _ x) (at level 20).
+  Notation "`  x" := (take_lev _ x).
   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
-  Notation "``` x" := ((drop_depth _ x)) (at level 20).
+  Notation "``` x" := ((drop_lev _ x)) (at level 20).
   Notation "!<[]> x" := (garrowfy_code_types _ x) (at level 1).
-  Notation "!<[@]>" := (garrowfy_leveled_code_types _) (at level 1).
+  Notation "!<[@]> x" := (mapOptionTree garrowfy_leveled_code_types x) (at level 1).
 *)
+
     destruct case_RLet.
       simpl.
       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
-      destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl.
       repeat drop_simplify.
       repeat take_simplify.
-      rename σ₁ into a.
-      rename σ₂ into b.
-      rewrite mapOptionTree_distributes.
-      rewrite mapOptionTree_distributes.
-      set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_depth (ec :: lev) Σ₁)) as A.
-      set (take_lev (ec :: lev) Σ₁) as A'.
-      set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_depth (ec :: lev) Σ₂)) as B.
-      set (take_lev (ec :: lev) Σ₂) as B'.
       simpl.
 
       eapply nd_comp.
-      Focus 2.
-      eapply nd_rule.
-      eapply RLet.
-
-      apply nd_prod.
-
-      apply boost.
-      apply ga_second.
-
-      eapply nd_comp.
-      Focus 2.
+      eapply nd_prod; [ idtac | apply nd_id ].
       eapply boost.
-      apply ga_comp.
+      apply ga_second.
 
       eapply nd_comp.
-      eapply nd_rule.
-      eapply RArrange.
-      eapply RCanR.
-
+      eapply nd_prod.
+      apply nd_id.
       eapply nd_comp.
-      Focus 2.
       eapply nd_rule.
       eapply RArrange.
-      eapply RExch.
-      idtac.
+      apply RCanR.
+      eapply precompose.
 
-      eapply nd_comp.
-      apply nd_llecnac.
-      eapply nd_comp.
-      Focus 2.
-      eapply nd_rule.
-      apply RJoin.
-      apply nd_prod.
-
-      eapply nd_rule.
-      eapply RVar.
-
-      apply nd_id.
+      apply nd_rule.
+      apply RLet.
 
     destruct case_RVoid.
       simpl.
@@ -737,7 +937,7 @@ Section HaskFlattener.
       apply RAppT.
       apply Δ.
       apply Δ.
-      apply (Prelude_error "AppT at depth>0").
+      apply (Prelude_error "found type application at level >0; this is not supported").
 
     destruct case_RAbsT.
       simpl. destruct lev; simpl.
@@ -745,8 +945,8 @@ Section HaskFlattener.
       rewrite garrowfy_commutes_with_HaskTApp.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
       simpl.
-      set (mapOptionTree (garrowfy_leveled_code_types n) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
-      set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types n) Σ)) as q'.
+      set (mapOptionTree (garrowfy_leveled_code_types ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
+      set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types ) Σ)) as q'.
       assert (a=q').
         unfold a.
         unfold q'.
@@ -765,7 +965,7 @@ Section HaskFlattener.
       apply nd_id.
       apply Δ.
       apply Δ.
-      apply (Prelude_error "AbsT at depth>0").
+      apply (Prelude_error "found type abstraction at level >0; this is not supported").
 
     destruct case_RAppCo.
       simpl. destruct lev; simpl.
@@ -775,22 +975,23 @@ Section HaskFlattener.
       apply RAppCo.
       apply flatten_coercion.
       apply γ.
-      apply (Prelude_error "AppCo at depth>0").
+      apply (Prelude_error "found coercion application at level >0; this is not supported").
 
     destruct case_RAbsCo.
       simpl. destruct lev; simpl.
       unfold garrowfy_code_types.
       simpl.
       apply (Prelude_error "AbsCo not supported (FIXME)").
-      apply (Prelude_error "AbsCo at depth>0").
+      apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
 
     destruct case_RLetRec.
       rename t into lev.
+      simpl.
       apply (Prelude_error "LetRec not supported (FIXME)").
 
     destruct case_RCase.
       simpl.
-      apply (Prelude_error "Case not supported (FIXME)").
+      apply (Prelude_error "Case not supported (BIG FIXME)").
       Defined.