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