X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=2ea0c4a1e4cfaea4311bcda04a7090166d87d53f;hp=6f75235f42e9b7ea04ea87dd7fb1b352cf1fef51;hb=171beb27508a340b24ab14837e72451d0b500805;hpb=539d675a181f178e24c15b2a6ad3c990492eed79

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 6f75235..2ea0c4a 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -6,6 +6,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
@@ -25,19 +26,13 @@ Section HaskProofToStrong.
 
   Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
 
-  Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type :=
-    match j with
-      mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars ->
-        FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
-      end.
-
   Definition judg2exprType (j:Judg) : Type :=
     match j with
-      (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
-        FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
+      (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
+        FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ)
       end.
 
-  Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ.
+  Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l.
     intros.
     inversion X; auto.
     Defined.
@@ -48,7 +43,7 @@ Section HaskProofToStrong.
     Defined.
 
   Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
-    update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q.
+    update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q.
     intros.
     induction l1.
       reflexivity.
@@ -125,11 +120,19 @@ Section HaskProofToStrong.
     reflexivity.
     Qed.
     
+  Lemma fresh_lemma'' Γ 
+    : forall types ξ lev, 
+    FreshM { varstypes : _
+      |  mapOptionTree (update_xi(Γ:=Γ)   ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
+      /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
+  admit.
+  Defined.
+
   Lemma fresh_lemma' Γ 
     : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
     FreshM { varstypes : _
-      |  mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
-      /\ mapOptionTree (update_ξ       ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
+      |  mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
+      /\ mapOptionTree (update_xi       ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
       /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
     induction types.
       intros; destruct a.
@@ -162,7 +165,7 @@ Section HaskProofToStrong.
         intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
           apply FreshMon.
           destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
-          refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev
+          refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev
             (leaves vt2)) _ _; return _).
           apply FreshMon.
           simpl.
@@ -202,8 +205,8 @@ Section HaskProofToStrong.
   Lemma fresh_lemma Γ ξ vars Σ Σ' lev
     : Σ = mapOptionTree ξ vars ->
     FreshM { vars' : _
-      |  mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
-      /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
+      |  mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
+      /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
     intros.
     set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
     refine (q >>>= fun q' => return _).
@@ -220,176 +223,140 @@ Section HaskProofToStrong.
       inversion pf2.
     Defined.
 
-  Definition urule2expr  : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
-    ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
-
-      refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} : 
-        ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
-        match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with
-          | RLeft   h c ctx r => let case_RLeft  := tt in (fun e => _) (urule2expr _ _ _ _ r)
-          | RRight  h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
-          | RCanL   t a       => let case_RCanL  := tt in _
-          | RCanR   t a       => let case_RCanR  := tt in _
-          | RuCanL  t a       => let case_RuCanL := tt in _
-          | RuCanR  t a       => let case_RuCanR := tt in _
-          | RAssoc  t a b c   => let case_RAssoc := tt in _
-          | RCossa  t a b c   => let case_RCossa := tt in _
-          | RExch   t a b     => let case_RExch  := tt in _
-          | RWeak   t a       => let case_RWeak  := tt in _
-          | RCont   t a       => let case_RCont  := tt in _
+  Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type :=
+    forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ).
+
+  Definition urule2expr  : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
+    ujudg2exprType Γ ξ Δ h t l ->
+    ujudg2exprType Γ ξ Δ j t l
+    .
+    intros Γ Δ.
+      refine (fix urule2expr h j t l (r:@Arrange _ h j) ξ {struct r} : 
+    ujudg2exprType Γ ξ Δ h t l ->
+    ujudg2exprType Γ ξ Δ j t l :=
+        match r as R in Arrange H C return
+    ujudg2exprType Γ ξ Δ H t l ->
+    ujudg2exprType Γ ξ Δ C t l
+ with
+          | ALeft   h c ctx r => let case_ALeft  := tt in (fun e => _) (urule2expr _ _ _ _ r)
+          | ARight  h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r)
+          | AId     a       => let case_AId    := tt in _
+          | ACanL   a       => let case_ACanL  := tt in _
+          | ACanR   a       => let case_ACanR  := tt in _
+          | AuCanL  a       => let case_AuCanL := tt in _
+          | AuCanR  a       => let case_AuCanR := tt in _
+          | AAssoc  a b c   => let case_AAssoc := tt in _
+          | AuAssoc  a b c   => let case_AuAssoc := tt in _
+          | AExch   a b     => let case_AExch  := tt in _
+          | AWeak   a       => let case_AWeak  := tt in _
+          | ACont   a       => let case_ACont  := tt in _
+          | AComp   a b c f g => let case_AComp  := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
           end); clear urule2expr; intros.
 
-      destruct case_RCanL.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 ([],,vars)).
+      destruct case_AId.
+        apply X.
+
+      destruct case_ACanL.
+        simpl; unfold ujudg2exprType; intros.
+        simpl in X.
+        apply (X ([],,vars)).
         simpl; rewrite <- H; auto.
 
-      destruct case_RCanR.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 (vars,,[])).
+      destruct case_ACanR.
+        simpl; unfold ujudg2exprType; intros.
+        simpl in X.
+        apply (X (vars,,[])).
         simpl; rewrite <- H; auto.
 
-      destruct case_RuCanL.
-        apply ILeaf; simpl; intros.
+      destruct case_AuCanL.
+        simpl; unfold ujudg2exprType; intros.
         destruct vars; try destruct o; inversion H.
-        inversion X.
-        simpl in X0.
-        apply (X0 vars2); auto.
+        simpl in X.
+        apply (X vars2); auto.
 
-      destruct case_RuCanR.
-        apply ILeaf; simpl; intros.
+      destruct case_AuCanR.
+        simpl; unfold ujudg2exprType; intros.
         destruct vars; try destruct o; inversion H.
-        inversion X.
-        simpl in X0.
-        apply (X0 vars1); auto.
-
-      destruct case_RAssoc.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
+        simpl in X.
+        apply (X vars1); auto.
+
+      destruct case_AAssoc.
+        simpl; unfold ujudg2exprType; intros.
+        simpl in X.
         destruct vars; try destruct o; inversion H.
         destruct vars1; try destruct o; inversion H.
-        apply (X0 (vars1_1,,(vars1_2,,vars2))).
+        apply (X (vars1_1,,(vars1_2,,vars2))).
         subst; auto.
 
-      destruct case_RCossa.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
+      destruct case_AuAssoc.
+        simpl; unfold ujudg2exprType; intros.
+        simpl in X.
         destruct vars; try destruct o; inversion H.
         destruct vars2; try destruct o; inversion H.
-        apply (X0 ((vars1,,vars2_1),,vars2_2)).
+        apply (X ((vars1,,vars2_1),,vars2_2)).
         subst; auto.
 
-      destruct case_RLeft.
-        destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
-        destruct o; [ idtac | apply INone ].
-        destruct u; simpl in *.
-        apply ILeaf; simpl; intros.
+      destruct case_AExch.
+        simpl; unfold ujudg2exprType ; intros.
+        simpl in X.
         destruct vars; try destruct o; inversion H.
-        set (fun q => ileaf (e ξ q)) as r'.
-        simpl in r'.
-        apply r' with (vars:=vars2).
-        clear r' e.
-        clear r0.
-        induction h0.
-          destruct a.
-          destruct u.
+        apply (X (vars2,,vars1)).
+        inversion H; subst; auto.
+        
+      destruct case_AWeak.
+        simpl; unfold ujudg2exprType; intros.
+        simpl in X.
+        apply (X []).
+        auto.
+        
+      destruct case_ACont.
+        simpl; unfold ujudg2exprType ; intros.
+        simpl in X.
+        apply (X (vars,,vars)).
+        simpl.
+        rewrite <- H.
+        auto.
+
+      destruct case_ALeft.
+        intro vars; unfold ujudg2exprType; intro H.
+        destruct vars; try destruct o; inversion H.
+        apply (fun q => e ξ q vars2 H2).
+        clear r0 e H2.
           simpl in X.
-          apply ileaf in X. 
-          apply ILeaf.
           simpl.
-          simpl in X.
+          unfold ujudg2exprType.
           intros.
           apply X with (vars:=vars1,,vars).
-          simpl.
           rewrite H0.
           rewrite H1.
+          simpl.
           reflexivity.
-          apply INone.
-          apply IBranch.
-          apply IHh0_1. inversion X; auto.
-          apply IHh0_2. inversion X; auto.
-          auto.
-        
-      destruct case_RRight.
-        destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
-        destruct o; [ idtac | apply INone ].
-        destruct u; simpl in *.
-        apply ILeaf; simpl; intros.
+
+      destruct case_ARight.
+        intro vars; unfold ujudg2exprType; intro H.
         destruct vars; try destruct o; inversion H.
-        set (fun q => ileaf (e ξ q)) as r'.
-        simpl in r'.
-        apply r' with (vars:=vars1).
-        clear r' e.
-        clear r0.
-        induction h0.
-          destruct a.
-          destruct u.
+        apply (fun q => e ξ q vars1 H1).
+        clear r0 e H2.
           simpl in X.
-          apply ileaf in X. 
-          apply ILeaf.
           simpl.
-          simpl in X.
+          unfold ujudg2exprType.
           intros.
           apply X with (vars:=vars,,vars2).
-          simpl.
           rewrite H0.
-          rewrite H2.
+          inversion H.
+          simpl.
           reflexivity.
-          apply INone.
-          apply IBranch.
-          apply IHh0_1. inversion X; auto.
-          apply IHh0_2. inversion X; auto.
-          auto.
-
-      destruct case_RExch.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        destruct vars; try destruct o; inversion H.
-        apply (X0 (vars2,,vars1)).
-        inversion H; subst; auto.
-        
-      destruct case_RWeak.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 []).
-        auto.
-        
-      destruct case_RCont.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 (vars,,vars)).
-        simpl.
-        rewrite <- H.
-        auto.
-        Defined.
 
-  Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ :
-    ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c.
-    intro it.
-    induction c.
-    destruct a.
-      destruct u; simpl in *.
-      apply ileaf in it.
-      apply ILeaf.
-      simpl in *.
-      intros; apply it with (vars:=vars); auto.
-    apply INone.
-    apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
-    Defined.
+      destruct case_AComp.
+        apply e2.
+        apply e1.
+        apply X.
+        Defined.
 
   Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
-    ITree (LeveledHaskType Γ ★)
-         (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
-         (mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
+    ITree (HaskType Γ ★)
+         (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l)
+         (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes)
          -> ELetRecBindings Γ Δ ξ' l varstypes.
     intros.
     induction varstypes.
@@ -405,6 +372,8 @@ Section HaskProofToStrong.
       simpl.
       destruct (eqd_dec h0 l).
         rewrite <- e0.
+        simpl in X.
+        subst.
         apply X.
       apply (Prelude_error "level mismatch; should never happen").
       apply (Prelude_error "letrec type mismatch; should never happen").
@@ -415,100 +384,374 @@ Section HaskProofToStrong.
       apply IHvarstypes2; inversion X; auto.
     Defined.
 
-  Definition case_helper tc Γ Δ lev tbranches avars ξ (Σ:Tree ??VV) :
-    forall pcb : ProofCaseBranch tc Γ Δ lev tbranches avars,
-    judg2exprType (pcb_judg pcb) ->
-    (pcb_freevars pcb) = mapOptionTree ξ Σ ->
-    FreshM
-    {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars &
-    Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars (weakCK'' Δ)) 
-    (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@  lev))}.
+  Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
+    refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
+      | INone => T_Leaf None
+      | ILeaf x y => T_Leaf (Some _)
+      | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
+            end).
+    exists x; auto.
+    Defined.
 
-    intros.
+  Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
+    :  ITree { x:X & F x } (fun x => J (projT1 x))                                t
+    -> ITree X             (fun x:X => J x)   (mapOptionTree (@projT1 _ _) t).
+    intro it.
+    induction it; simpl in *.
+    apply INone.
+    apply ILeaf.
+    apply f.
+    simpl; apply IBranch; auto.
+    Defined.
+
+  Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
+    refine (fix rec t := match t with
+      | T_Leaf None => T_Leaf None
+      | T_Leaf (Some x) => T_Leaf (Some _)
+      | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
+            end).
+    destruct x as [x fx].
+    refine (bind fx' = fx ; return _).
+    apply FreshMon.
+    exists x.
+    apply fx'.
+    Defined.
+  
+  Definition case_helper tc Γ Δ lev tbranches avars ξ :
+    forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
+     prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
+     ((fun sac => FreshM
+       { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
+         & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
+         (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
+    intro pcb.
+    intro X.
     simpl in X.
-    destruct pcb.
+    simpl.
+    destruct pcb as [sac pcb].
     simpl in *.
-    set (sac_types pcb_scb _ avars) as boundvars.
-    refine (fresh_lemma' _ (unleaves (vec2list boundvars)) Σ (mapOptionTree weakLT' pcb_freevars) (weakLT' ○ ξ) (weakL' lev) _
-      >>>= fun ξvars => _). apply FreshMon.
-    rewrite H.
-    rewrite <- mapOptionTree_compose.
-    reflexivity.
-      destruct ξvars as [ exprvars [pf1 [pf2 pfdistinct]]].
-      set (list2vec (leaves (mapOptionTree (@fst _ _) exprvars))) as exprvars'. 
-
-   assert (distinct (vec2list exprvars')) as pfdistinct'.
-     unfold exprvars'.
-     rewrite vec2list_list2vec.
-     apply pfdistinct.
-
-      assert (sac_numExprVars pcb_scb = Datatypes.length (leaves (mapOptionTree (@fst _ _) exprvars))) as H'.
-        rewrite <- mapOptionTree_compose in pf2.
-        simpl in pf2.
-        rewrite mapleaves.
-        rewrite <- map_preserves_length.
-        rewrite map_preserves_length with (f:=
-          (@update_ξ VV eqdec_vv (@sac_Γ tc pcb_scb Γ)
-            (@weakLT' Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) ★ ○ ξ)
-            (@weakL'  Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) lev)
-            (@leaves (VV * HaskType (@sac_Γ tc pcb_scb Γ) ★) exprvars) ○ @fst VV (HaskType (@sac_Γ tc pcb_scb Γ) ★))).
-        rewrite <- mapleaves.
-        rewrite pf2.       
-        rewrite <- mapleaves'.
-        rewrite leaves_unleaves.
-        rewrite vec2list_map_list2vec.
-        rewrite vec2list_len.
-        reflexivity.
-
-        clear pfdistinct'.
-     rewrite <- H' in exprvars'.
-       clear H'.
-   assert (distinct (vec2list exprvars')) as pfdistinct'.
-     admit.
-
-   set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars' pfdistinct') as scb.
-      set (scbwv_ξ scb ξ lev) as ξ'.
-      refine (X ξ' (Σ,,(unleaves (vec2list exprvars'))) _ >>>= fun X' => return _). apply FreshMon.
+
+    destruct X.
+    destruct s as [vars vars_pf].
+
+    refine (bind localvars = fresh_lemma' _ (unleaves  (vec2list (sac_types sac _ avars))) vars 
+      (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _  ; _).
+      apply FreshMon.
+      rewrite vars_pf.
+      rewrite <- mapOptionTree_compose.
+      reflexivity.
+      destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
+      set (mapOptionTree (@fst _ _) localvars) as localvars'.
+
+    set (list2vec (leaves localvars')) as localvars''.
+    cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
+      rewrite H'' in localvars''.
+    cut (distinct (vec2list localvars'')). intro H'''.
+    set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
+
+    refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
+      apply FreshMon.
       simpl.
-      unfold ξ'.
-      unfold scbwv_ξ.
+      unfold scbwv_xi.
+      rewrite vars_pf.
+      rewrite <- mapOptionTree_compose.
+      clear localvars_pf1.
       simpl.
-      admit.
-
-    apply ileaf in X'.
-      simpl in X'.
-      exists scb.
-      unfold weakCK''.
-      unfold ξ' in X'.
-      apply X'.
+      rewrite mapleaves'.
+
+    admit.
+
+    exists scb.
+    apply ileaf in q.
+    apply q.
+
+    admit.
+    admit.
     Defined.
 
-  Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
-    match t with
-      | T_Leaf None     => return []
-      | T_Leaf (Some x) => bind x' = x ; return [x']
-      | T_Branch b1 b2  => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
-    end.
+  Definition gather_branch_variables
+    Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
+                ProofCaseBranch tc Γ Δ lev tbranches avars sac})
+    :
+    forall vars,
+    mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
+    -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
+    -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q))) 
+      { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
+  alts.
+    induction alts;
+    intro vars;
+    intro pf;
+    intro source.
+    destruct a; [ idtac | apply INone ].
+    simpl in *.
+    apply ileaf in source.
+    apply ILeaf.
+    destruct s as [sac pcb].
+    simpl in *.
+    split.
+    intros.
+    eapply source.
+    apply H.
+    clear source.
+
+    exists vars.
+    auto.
+
+    simpl in pf.
+    destruct vars; try destruct o; simpl in pf; inversion pf.
+    simpl in source.
+    inversion source.
+    subst.
+    apply IBranch.
+    apply (IHalts1 vars1 H0 X); auto.
+    apply (IHalts2 vars2 H1 X0); auto.
+
+    Defined.
 
-  Lemma itree_mapOptionTree : forall T T' F (f:T->T') t,
-    ITree _ F (mapOptionTree f t) ->
-    ITree _ (F ○ f) t.
+  Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
+    FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
+    intros Γ Σ.
+    induction Σ; intro ξ.
+    destruct a.
+    destruct l as [τ l].
+    set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
+    refine (q >>>= fun q' => return _).
+    apply FreshMon.
+    clear q.
+    destruct q' as [varstypes [pf1 [pf2 distpf]]].
+    exists (mapOptionTree (@fst _ _) varstypes).
+    exists (update_xi ξ l (leaves varstypes)).
+    symmetry; auto.
+    refine (return _).
+    exists [].
+    exists ξ; auto.
+    refine (bind f1 = IHΣ1 ξ ; _).
+    apply FreshMon.
+    destruct f1 as [vars1 [ξ1 pf1]].
+    refine (bind f2 = IHΣ2 ξ1 ; _).
+    apply FreshMon.
+    destruct f2 as [vars2 [ξ2 pf22]].
+    refine (return _).
+    exists (vars1,,vars2).
+    exists ξ2.
+    simpl.
+    rewrite pf22.
+    rewrite pf1.
+    admit.         (* freshness assumption *)
+    Defined.
+
+  Definition rlet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p :
+    forall (X_ : ITree Judg judg2exprType
+         ([Γ > Δ > Σ₁ |- [σ₁] @ p],, [Γ > Δ > [σ₁ @@  p],, Σ₂ |- [σ₂] @ p])),
+   ITree Judg judg2exprType [Γ > Δ > Σ₁,, Σ₂ |- [σ₂] @ p].
     intros.
-    induction t; try destruct a; simpl in *.
-      apply ILeaf.
-      inversion X; auto.
-      apply INone.
-      apply IBranch.
-        apply IHt1; inversion X; auto.
-        apply IHt2; inversion X; auto.
-        Defined.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+
+    refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
+    apply FreshMon.
+
+    destruct pf as [ vnew [ pf1 pf2 ]].
+    set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
+    inversion X_.
+    apply ileaf in X.
+    apply ileaf in X0.
+    simpl in *.
+
+    refine (X ξ vars1 _ >>>= fun X0' => _).
+    apply FreshMon.
+    simpl.
+    auto.
+
+    refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
+    apply FreshMon.
+    simpl.
+    rewrite pf2.
+    rewrite pf1.
+    reflexivity.
+    apply FreshMon.
+
+    apply ILeaf.
+    apply ileaf in X1'.
+    apply ileaf in X0'.
+    simpl in *.
+    apply ELet with (ev:=vnew)(tv:=σ₁).
+    apply X0'.
+    apply X1'.
+    Defined.
+
+  Definition vartree Γ Δ Σ lev ξ :
+    forall vars, Σ @@@ lev = mapOptionTree ξ vars ->
+    ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ.
+    induction Σ; intros.
+    destruct a.
+    intros; simpl in *.
+    apply ILeaf.
+    destruct vars; try destruct o; inversion H.
+    set (EVar Γ Δ ξ v) as q.
+    rewrite <- H1 in q.
+    apply q.
+    intros.
+    apply INone.
+    intros.
+    destruct vars; try destruct o; inversion H.
+    apply IBranch.
+    eapply IHΣ1.
+    apply H1.
+    eapply IHΣ2.
+    apply H2.
+    Defined.
+
+
+  Definition rdrop  Γ Δ Σ₁ Σ₁₂ a lev :
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *.
+    intros.
+    set (X ξ vars H) as q.
+    simpl in q.
+    refine (q >>>= fun q' => return _).
+    apply FreshMon.
+    inversion q'.
+    apply X0.
+    Defined.
+
+  Definition rdrop'  Γ Δ Σ₁ Σ₁₂ a lev :
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *.
+    intros.
+    set (X ξ vars H) as q.
+    simpl in q.
+    refine (q >>>= fun q' => return _).
+    apply FreshMon.
+    inversion q'.
+    auto.
+    Defined.
+
+  Definition rdrop''  Γ Δ Σ₁ Σ₁₂ lev :
+    ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    eapply X with (vars:=[],,vars).
+    rewrite H; reflexivity.
+    Defined.
+
+  Definition rdrop'''  Γ Δ a Σ₁ Σ₁₂ lev :
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+    eapply X with (vars:=vars2).
+    auto.
+    Defined.
+
+  Definition rassoc  Γ Δ Σ₁ a b c lev :
+    ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+    destruct vars2; try destruct o; inversion H2.
+    apply X with (vars:=(vars1,,vars2_1),,vars2_2).
+    subst; reflexivity.
+    Defined.
+
+  Definition rassoc'  Γ Δ Σ₁ a b c lev :
+    ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+    destruct vars1; try destruct o; inversion H1.
+    apply X with (vars:=vars1_1,,(vars1_2,,vars2)).
+    subst; reflexivity.
+    Defined.
+
+  Definition swapr  Γ Δ Σ₁ a b c lev :
+    ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+    destruct vars1; try destruct o; inversion H1.
+    apply X with (vars:=(vars1_2,,vars1_1),,vars2).
+    subst; reflexivity.
+    Defined.
+
+  Definition rdup  Γ Δ Σ₁ a  c lev :
+    ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+    apply X with (vars:=(vars1,,vars1),,vars2).    (* is this allowed? *)
+    subst; reflexivity.
+    Defined.
+
+  (* holy cow this is ugly *)
+  Definition rcut Γ Δ  Σ₃ lev  Σ₁₂  :
+    forall Σ₁ Σ₂,
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |-  Σ₁₂ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ >  Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev].
+
+    induction Σ₁₂.
+    intros.
+    destruct a.
+
+    eapply rlet.
+    apply IBranch.
+    apply X.
+    apply X0.
+
+    simpl in X0.
+    apply rdrop'' in X0.
+    apply rdrop'''.
+    apply X0.
+
+    intros.
+    simpl in X0.
+    apply rassoc in X0.
+    set (IHΣ₁₂1 _ _ (rdrop  _ _ _ _ _ _ X) X0) as q.
+    set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'.
+    apply rassoc' in q.
+    apply swapr in q.
+    apply rassoc in q.
+    set (q' q) as q''.
+    apply rassoc' in q''.
+    apply rdup in q''.
+    apply q''.
+    Defined.
 
   Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
 
     intros h j r.
 
       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
-      | RURule a b c d e              => let case_RURule := tt        in _
+      | RArrange a b c d e l r        => let case_RURule := tt        in _
       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
@@ -521,27 +764,27 @@ Section HaskProofToStrong.
       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
-      | RBindingGroup Γ p lri m x q   => let case_RBindingGroup := tt in _
-      | REmptyGroup _ _               => let case_REmptyGroup := tt   in _
+      | RCut    Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l    => let case_RCut := tt          in _
+      | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
+      | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
+      | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _
+      | RVoid   _ _ l                 => let case_RVoid := tt   in _
       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
       | REsc    Σ a b c n m           => let case_REsc := tt          in _
       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
       end); intro X_; try apply ileaf in X_; simpl in X_.
 
-  destruct case_RURule.
-    destruct d; try destruct o.
-      apply ILeaf; destruct u; simpl; intros.
-      set (@urule2expr a b _ _ e ξ) as q.
-      set (fun z => ileaf (q z)) as q'.
-      simpl in q'.
-      apply q' with (vars:=vars).
-      clear q' q.
-      apply bridge.
-      apply X_.
+    destruct case_RURule.
+      apply ILeaf. simpl. intros.
+      set (@urule2expr a b _ _ e l r0 ξ) as q.
+      unfold ujudg2exprType.
+      unfold ujudg2exprType in q.
+      apply q with (vars:=vars).
+      intros.
+      apply X_ with (vars:=vars0).
+      auto.
       auto.
-      apply no_urules_with_empty_conclusion in e; inversion e; auto.
-      apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
 
   destruct case_RBrak.
     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
@@ -564,14 +807,16 @@ Section HaskProofToStrong.
 
   destruct case_RVar.
     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
-    destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
-    apply EVar.
+    destruct vars; simpl in H; inversion H; destruct o. inversion H1.
+    set (@EVar _ _ _ Δ ξ v) as q.
+    rewrite <- H2 in q.
+    simpl in q.
+    apply q.
     inversion H.
 
   destruct case_RGlobal.
     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
     apply EGlobal.
-    apply wev.
 
   destruct case_RLam.
     apply ILeaf.
@@ -579,7 +824,7 @@ Section HaskProofToStrong.
     refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
     apply FreshMon.
     destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_ξ ξ x ((⟨vnew, tx  ⟩) :: nil)) as ξ' in *.
+    set (update_xi ξ x (((vnew, tx  )) :: nil)) as ξ' in *.
     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
     apply FreshMon.
     simpl.
@@ -603,19 +848,6 @@ Section HaskProofToStrong.
     apply ileaf in X. simpl in X.
     apply X.
 
-  destruct case_RBindingGroup.
-    apply ILeaf; simpl; intros.
-    inversion X_.
-    apply ileaf in X.
-    apply ileaf in X0.
-    simpl in *.
-    destruct vars; inversion H.
-    destruct o; inversion H3.
-    refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
-    apply FreshMon.
-    apply FreshMon.
-    apply IBranch; auto.
-
   destruct case_RApp.    
     apply ILeaf.
     inversion X_.
@@ -638,38 +870,101 @@ Section HaskProofToStrong.
     apply (EApp _ _ _ _ _ _ q1' q2').
 
   destruct case_RLet.
+    eapply rlet.
+    apply X_.
+
+  destruct case_RWhere.
     apply ILeaf.
     simpl in *; intros.
-    destruct vars; try destruct o; inversion H.
-    refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
+    destruct vars;  try destruct o; inversion H.
+    destruct vars2; try destruct o; inversion H2.
+    clear H2.
+
+    assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
+    refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
     apply FreshMon.
+
     destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_ξ ξ p ((⟨vnew, σ₂  ⟩) :: nil)) as ξ' in *.
+    set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
     inversion X_.
     apply ileaf in X.
     apply ileaf in X0.
     simpl in *.
-    refine (X0 ξ  vars2 _ >>>= fun X0' => _).
-    apply FreshMon.
-    auto.
-    refine (X  ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
+
+    refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
     apply FreshMon.
-    rewrite H1.
     simpl.
+    inversion pf1.
+    rewrite H3.
+    rewrite H4.
     rewrite pf2.
-    rewrite pf1.
-    rewrite H1.
     reflexivity.
-    refine (return _).
+
+    refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
+    apply FreshMon.
+    reflexivity.
+    apply FreshMon.
+
     apply ILeaf.
     apply ileaf in X0'.
     apply ileaf in X1'.
     simpl in *.
-    apply ELet with (ev:=vnew)(tv:=σ₂).
-    apply X0'.
+    apply ELet with (ev:=vnew)(tv:=σ₁).
     apply X1'.
+    apply X0'.
+
+  destruct case_RCut.
+    inversion X_.
+    subst.
+    clear X_.
+    induction Σ₃.
+    destruct a.
+    subst.
+    eapply rcut.
+    apply X.
+    apply X0.
+
+    apply ILeaf.
+    simpl.
+    intros.
+    refine (return _).
+    apply INone.
+    set (IHΣ₃1 (rdrop  _ _ _ _ _ _ X0)) as q1.
+    set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2.
+    apply ileaf in q1.
+    apply ileaf in q2.
+    simpl in *.
+    apply ILeaf.
+    simpl.
+    intros.
+    refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _).
+    apply FreshMon.
+    apply FreshMon.
+    apply IBranch; auto.
+
+  destruct case_RLeft.
+    apply ILeaf.
+    simpl; intros.
+    destruct vars; try destruct o; inversion H.
+    refine (X_ _ _ H2 >>>= fun X' => return _).
+    apply FreshMon.
+    apply IBranch.
+    eapply vartree.
+    apply H1.
+    apply X'.
+
+  destruct case_RRight.
+    apply ILeaf.
+    simpl; intros.
+    destruct vars; try destruct o; inversion H.
+    refine (X_ _ _ H1 >>>= fun X' => return _).
+    apply FreshMon.
+    apply IBranch.
+    apply X'.
+    eapply vartree.
+    apply H2.
 
-  destruct case_REmptyGroup.
+  destruct case_RVoid.
     apply ILeaf; simpl; intros.
     refine (return _).
     apply INone.
@@ -705,7 +1000,7 @@ Section HaskProofToStrong.
     apply ILeaf; simpl; intros.
     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
-    refine (X_ ((update_ξ ξ t (leaves varstypes)))
+    refine (X_ ((update_xi ξ t (leaves varstypes)))
       (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
     simpl.
     rewrite pf2.
@@ -715,12 +1010,21 @@ Section HaskProofToStrong.
     inversion X; subst; clear X.
 
     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+    auto.
     apply (@letrec_helper Γ Δ t varstypes).
-    rewrite <- pf2 in X1.
     rewrite mapOptionTree_compose.
+    rewrite mapOptionTree_compose.
+    rewrite pf2.
+    replace ((mapOptionTree unlev (y @@@ t))) with y.
+      apply X0.
+      clear pf1 X0 X1 pfdist pf2 vars varstypes.
+      induction y; try destruct a; auto.
+      rewrite IHy1 at 1.
+      rewrite IHy2 at 1.
+      reflexivity.
+    apply ileaf in X1.
+    simpl in X1.
     apply X1.
-    apply ileaf in X0.
-    apply X0.
 
   destruct case_RCase.
     apply ILeaf; simpl; intros.
@@ -729,76 +1033,47 @@ Section HaskProofToStrong.
     subst.
     apply ileaf in X0.
     simpl in X0.
-    set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *.
-    refine (bind ξvars = fresh_lemma' _ (mapOptionTree unlev (Σalts,,Σ)) _ _ _ lev H ; _).
-      apply FreshMon.
-      destruct vars; try destruct o; inversion H; clear H.
-      rename vars1 into varsalts.
-      rename vars2 into varsΣ.
 
-    refine ( _ >>>= fun Y => X0 ξ varsΣ _ >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
+    (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
+     * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
+    rename Σ into body_freevars_types.
+    rename vars into all_freevars.
+    rename X0 into body_expr.
+    rename X  into alts_exprs.
+
+    destruct all_freevars; try destruct o; inversion H.
+    rename all_freevars2 into body_freevars.
+    rename all_freevars1 into alts_freevars.
+
+    set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
+    set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
+    apply fix_indexing in alts_exprs'.
+    simpl in alts_exprs'.
+    apply unindex_tree in alts_exprs'.
+    simpl in alts_exprs'.
+    apply fix2 in alts_exprs'.
+    apply treeM in alts_exprs'.
+
+    refine ( alts_exprs' >>>= fun Y =>
+      body_expr ξ _ _
+      >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
       apply FreshMon.
-      destruct ξvars as [varstypes [pf1 pf2]].
-
-      apply treeM.
-      apply itree_mapOptionTree in X.
-      refine (itree_to_tree (itmap _ X)).
-      intros.
-      eapply case_helper.
-      apply X1.
-      instantiate (1:=varsΣ).
-      rewrite <- H2.
-      admit.
       apply FreshMon.
+      apply H2.
     Defined.
 
-  Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
-    refine ((
-      fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
-      match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
-      | cnd_weak             => let case_nil    := tt in INone _ _
-      | cnd_rule h c cnd' r  => let case_rule   := tt in rule2expr _ _ r (closed2expr' _ cnd')
-      | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
-      end)); clear closed2expr'; intros; subst.
-        Defined.
-
-  Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
-    FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
-    intros Γ Σ.
-    induction Σ; intro ξ.
-    destruct a.
-    destruct l as [τ l].
-    set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
-    refine (q >>>= fun q' => return _).
-    apply FreshMon.
-    clear q.
-    destruct q' as [varstypes [pf1 [pf2 distpf]]].
-    exists (mapOptionTree (@fst _ _) varstypes).
-    exists (update_ξ ξ l (leaves varstypes)).
-    symmetry; auto.
-    refine (return _).
-    exists [].
-    exists ξ; auto.
-    refine (bind f1 = IHΣ1 ξ ; _).
-    apply FreshMon.
-    destruct f1 as [vars1 [ξ1 pf1]].
-    refine (bind f2 = IHΣ2 ξ1 ; _).
-    apply FreshMon.
-    destruct f2 as [vars2 [ξ2 pf22]].
-    refine (return _).
-    exists (vars1,,vars2).
-    exists ξ2.
-    simpl.
-    rewrite pf22.
-    rewrite pf1.
-    admit.
-    Defined.
+  Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
+    match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
+    | scnd_weak   _             => let case_nil    := tt in fun _ => INone _ _
+    | scnd_comp   x h c cnd' r  => let case_rule   := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
+    | scnd_branch _ _ _ c1 c2   => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
+    end.
 
-  Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
-    {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
-    FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
+  Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
+    {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
+    FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
     intro pf.
-    set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
+    set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
     apply closed2expr in cnd.
     apply ileaf in cnd.
     simpl in *.
@@ -812,7 +1087,10 @@ Section HaskProofToStrong.
     auto.
     refine (return OK _).
     exists ξ.
-    apply (ileaf it).
+    apply ileaf in it.
+    simpl in it.
+    apply it.
+    apply INone.
     Defined.
 
 End HaskProofToStrong.