X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=1f1229d66651b2a6d24a74fac77524b85242fdd0;hp=3798a36fa341888940a05b0c0c9b888ebfb8bdff;hb=d97b00a6ff6e8e2244927d17bda4b9762fc3d716;hpb=8efffc7368b5e54c42461f45a9708ff2828409a4

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 3798a36..1f1229d 100644
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -6,143 +6,573 @@ 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.
 Require Import HaskKinds.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
-Require Import HaskWeakVars.
 Require Import HaskProof.
 
 Section HaskStrongToProof.
+ 
+Context {VV:Type}{eqd_vv:EqDecidable VV}.
 
-(* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform
- * expansion on an entire uniform proof *)
-Definition ext_left  {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
-  := @nd_map' _ _ _ _ (ext_tree_left ctx)  (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)).
-Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
-  := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)).
-
-Definition pivotContext {Γ}{Δ} a b c τ :
-  @ND _ (@URule Γ Δ)
-    [ Γ >> Δ > (a,,b),,c |- τ]
-    [ Γ >> Δ > (a,,c),,b |- τ].
-  set (ext_left a _ _ (nd_rule (@RExch Γ Δ τ c b))) as q.
-  simpl in *.
-  eapply nd_comp ; [ eapply nd_rule; apply RCossa | idtac ]. 
-  eapply nd_comp ; [ idtac | eapply nd_rule; apply RAssoc ].
-  apply q.
-  Defined.
+(* maintenance of Xi *)
+Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
+  match lv with
+    | nil     => Some v
+    | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
+  end.
 
-Definition copyAndPivotContext {Γ}{Δ} a b c τ :
-  @ND _ (@URule Γ Δ)
-    [ Γ >> Δ > (a,,b),,(c,,b) |- τ]
-    [ Γ >> Δ > (a,,c),,b |- τ].
-    set (ext_left (a,,c) _ _ (nd_rule (@RCont Γ Δ τ b))) as q.
-    simpl in *.
-    eapply nd_comp; [ idtac | apply q ].
-    clear q.
-    eapply nd_comp ; [ idtac | eapply nd_rule; apply RCossa ].
-    set (ext_right b _ _ (@pivotContext _ Δ a b c τ)) as q.
+Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
+  match t with 
+    | T_Leaf None     => T_Leaf None
+    | T_Leaf (Some x) => T_Leaf (f x)
+    | T_Branch l r    => T_Branch (mapOptionTree' f l) (mapOptionTree' f r)
+  end.
+
+  (* later: use mapOptionTreeAndFlatten *)
+  Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
+    mapOptionTree' (dropVar lv).
+
+Lemma In_both : forall T (l1 l2:list T) a, In a l1 -> In a (app l1 l2).
+  intros T l1.
+  induction l1; intros.
+  inversion H.
+  simpl.
+  inversion H; subst.
+  left; auto.
+  right.
+  apply IHl1.
+  apply H0.
+  Qed.
+
+Lemma In_both' : forall T (l1 l2:list T) a, In a l2 -> In a (app l1 l2).
+  intros T l1.
+  induction l1; intros.
+  apply H.
+  rewrite <- app_comm_cons.
+  simpl.
+  right.
+  apply IHl1.
+  auto.
+  Qed.
+
+Lemma distinct_app : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1 /\ distinct l2.
+  intro T.
+  intro l1.
+  induction l1; intros.
+  split; auto.
+  apply distinct_nil.
+  simpl in H.
+  inversion H.
+  subst.
+  set (IHl1 _ H3) as H3'.
+  destruct H3'.
+  split; auto.
+  apply distinct_cons; auto.
+  intro.
+  apply H2.
+  apply In_both; auto.
+  Qed.
+
+Lemma mapOptionTree'_compose : forall T A B (t:Tree ??T) (f:T->??A)(g:A->??B),
+  mapOptionTree' g (mapOptionTree' f t)
+  = 
+  mapOptionTree' (fun x => match f x with None => None | Some x => g x end) t.
+  intros; induction t.
+    destruct a; auto.
+    simpl.
+    destruct (f t); reflexivity.
+    simpl.
+    rewrite <- IHt1.
+    rewrite <- IHt2.
+    reflexivity.
+    Qed.
+
+Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t).
+  unfold stripOutVars.
+  rewrite mapOptionTree'_compose.
+  simpl.
+  induction t.
+  destruct a0.
+  simpl.
+  induction x.
+  reflexivity.
+  simpl.
+  destruct (eqd_dec v a0).
+    destruct (eqd_dec v a); reflexivity.
+    apply IHx.
+  reflexivity.
+  simpl.
+  rewrite <- IHt1.
+  rewrite <- IHt2.
+  reflexivity.
+  Qed.
+
+Lemma strip_nil_lemma       t : stripOutVars nil t = t.
+  induction t; simpl.
+  unfold stripOutVars.
+    destruct a; reflexivity.
+    rewrite <- IHt1 at 2.
+    rewrite <- IHt2 at 2.
+    reflexivity.
+    Qed.
+
+Lemma strip_swap0_lemma : forall a a0 y t,
+  stripOutVars (a :: a0 :: y) t = stripOutVars (a0 :: a :: y) t.
+  intros.
+  unfold stripOutVars.
+  induction t.
+  destruct a1; simpl; [ idtac | reflexivity ].
+  destruct (eqd_dec v a); subst.
+  destruct (eqd_dec a a0); subst.
+    reflexivity.
+    reflexivity.
+  destruct (eqd_dec v a0); subst.
+    reflexivity.
+    reflexivity.
     simpl in *.
-    eapply nd_comp ; [ idtac | apply q ]. 
-    clear q.
-    apply nd_rule.
-    apply RAssoc.
-    Defined.
+    rewrite IHt1.
+    rewrite IHt2.
+    reflexivity.
+    Qed.
 
+Lemma strip_swap1_lemma : forall a y t,
+  stripOutVars (a :: nil) (stripOutVars y t) =
+  stripOutVars y (stripOutVars (a :: nil) t).
+  intros.
+  induction y.
+    rewrite strip_nil_lemma.
+    rewrite strip_nil_lemma.
+    reflexivity.
+  rewrite (strip_lemma a0 y (stripOutVars (a::nil) t)).
+    rewrite <- IHy.
+    clear IHy.
+    rewrite <- (strip_lemma a y t).
+    rewrite <- strip_lemma.
+    rewrite <- strip_lemma.
+    apply strip_swap0_lemma.
+    Qed.
 
-  
-Context {VV:Type}{eqd_vv:EqDecidable VV}.
+Lemma strip_swap_lemma : forall  x y t, stripOutVars x (stripOutVars y t) = stripOutVars y (stripOutVars x t).
+  intros; induction t.
+    destruct a; simpl.
+
+    induction x.
+      rewrite strip_nil_lemma.
+        rewrite strip_nil_lemma.
+        reflexivity.
+      rewrite strip_lemma.
+        rewrite (strip_lemma a x [v]).
+        rewrite IHx.
+        clear IHx.
+        apply strip_swap1_lemma.
+    reflexivity.
+  unfold stripOutVars in *.
+    simpl.
+    rewrite IHt1.
+    rewrite IHt2.
+    reflexivity.
+  Qed.
 
-  (* maintenance of Xi *)
-  Definition dropVar (lv:list VV)(v:VV) : ??VV :=
-    if fold_left
-      (fun a b:bool => if a then true else if b then true else false)
-      (map (fun lvv => if eqd_dec lvv v then true else false) lv)
-      false
-      then None
-      else Some v.
-  (* later: use mapOptionTreeAndFlatten *)
-  Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
-    mapTree (fun x => match x with None => None | Some vt => dropVar lv vt end).
+Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app x y) t.
+  induction x; simpl.
+    apply strip_nil_lemma.
+    rewrite strip_lemma.
+    rewrite IHx.
+    clear IHx.
+    rewrite <- strip_lemma.
+    reflexivity.
+    Qed.
+
+Lemma notin_strip_inert a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
+  intros.
+  induction y.
+  destruct a0; try reflexivity.
+  simpl in *.
+  unfold stripOutVars.
+  simpl.
+  destruct (eqd_dec v a).
+  subst.
+  assert False.
+  apply H.
+  left; auto.
+  inversion H0.
+  auto.
+  rewrite <- IHy1 at 2.
+  rewrite <- IHy2 at 2.
+  reflexivity.
+  unfold not; intro.
+  apply H.
+  eapply In_both' in H0.
+  apply H0.
+  unfold not; intro.
+  apply H.
+  eapply In_both in H0.
+  apply H0.
+  Qed.
+
+Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v.
+  intros.
+  induction x.
+  reflexivity.
+  simpl.
+  destruct (eqd_dec v a).
+  subst.
+  assert False. apply H.
+  simpl; auto.
+  inversion H0.
+  apply IHx.
+  unfold not.
+  intro.
+  apply H.
+  simpl; auto.
+  Qed.
+
+Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c).
+  induction a; intros.
+  simpl.
+  simpl in H.
+  apply In_both'.
+  auto.
+  rewrite <- ass_app.
+  rewrite <- app_comm_cons.
+  simpl.
+  rewrite ass_app.
+  rewrite <- app_comm_cons in H.
+  inversion H.
+  left; auto.
+  right.
+  apply IHa.
+  apply H0.
+  Qed.
+
+Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c).
+  induction a; intros.
+  simpl in *.
+  apply distinct_app in H; auto.
+  destruct H; auto.
+  rewrite <- app_comm_cons.
+  apply distinct_cons.
+  rewrite <- ass_app in H.
+  rewrite <- app_comm_cons in H.
+  inversion H.
+  subst.
+  intro q.
+  apply H2.
+  rewrite ass_app.
+  apply in3.
+  auto.
+  apply IHa.
+  rewrite <- ass_app.
+  rewrite <- ass_app in H.
+  rewrite <- app_comm_cons in H.
+  inversion H.
+  subst.
+  auto.
+  Qed.
 
-Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
-  match exp as E in Expr Γ Δ ξ τ with
+Lemma notin_strip_inert' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
+  induction x; intros.
+  simpl in H.
+  unfold stripOutVars.
+  simpl.
+  induction y; try destruct a; auto.
+  simpl.
+  rewrite IHy1.
+  rewrite IHy2.
+  reflexivity.
+  simpl in H.
+  apply distinct_app in H; destruct H; auto.
+  apply distinct_app in H; destruct H; auto.
+  rewrite <- app_comm_cons in H.
+  inversion H; subst.
+  set (IHx H3) as qq.
+  rewrite strip_lemma.
+  rewrite IHx.
+  apply notin_strip_inert.
+  unfold not; intros.
+  apply H2.
+  apply In_both'.
+  auto.
+  auto.
+  Qed.
+
+Lemma dropvar_lemma v v' y : dropVar y v = Some v' -> v=v'.
+  intros.
+  induction y; auto.
+  simpl in H.
+  inversion H.
+  auto.
+  apply IHy.
+  simpl in H.
+  destruct (eqd_dec v a).
+  inversion H.
+  auto.
+  Qed.
+
+Lemma updating_stripped_tree_is_inert'
+  {Γ} lev
+  (ξ:VV -> LeveledHaskType Γ ★)
+  lv tree2 :
+    mapOptionTree (update_xi ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
+  = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
+
+  induction tree2.
+    destruct a; [ idtac | reflexivity ]; simpl.
+    induction lv; [ reflexivity | idtac ]; simpl.
+    destruct a; simpl.
+    set (eqd_dec v v0) as q; destruct q; auto.
+    set (dropVar (map (@fst _ _) lv) v) as b in *.
+      assert (dropVar (map (@fst _ _) lv) v=b). reflexivity.
+      destruct b; [ idtac | reflexivity ].
+      apply dropvar_lemma in H.
+      subst.
+      inversion IHlv.
+      rewrite H0.
+      clear H0 IHlv.
+      destruct (eqd_dec v0 v1).
+      subst.
+      assert False. apply n. intros; auto. inversion H.
+      reflexivity.
+    unfold stripOutVars in *.
+      simpl.
+      rewrite <- IHtree2_1.
+      rewrite <- IHtree2_2.
+      reflexivity.
+    Qed.
+
+Lemma distinct_bogus : forall {T}a0 (a:list T), distinct (a0::(app a (a0::nil))) -> False.
+  intros; induction a; auto.
+  simpl in H.
+  inversion H; subst.
+  apply H2; auto.
+  unfold In; simpl.
+  left; auto.
+  apply IHa.
+  clear IHa.
+  rewrite <- app_comm_cons in H.
+  inversion H; subst.
+  inversion H3; subst.
+  apply distinct_cons; auto.
+  intros.
+  apply H2.
+  simpl.
+  right; auto.
+  Qed.
+
+Lemma distinct_swap' : forall {T}a (b:list T), distinct (app b (a::nil)) -> distinct (a::b).
+  intros.
+  apply distinct_cons.
+    induction b; intros; simpl; auto.
+    rewrite <- app_comm_cons in H.
+    inversion H; subst.
+    set (IHb H4) as H4'.
+    apply H4'.
+    inversion H0; subst; auto.
+    apply distinct_bogus in H; inversion H.
+  induction b; intros; simpl; auto.
+    apply distinct_nil.
+    apply distinct_app in H.
+    destruct H; auto.
+  Qed.
+
+Lemma in_both : forall {T}(a b:list T) x, In x (app a b) -> In x a \/ In x b.
+  induction a; intros; simpl; auto.
+  rewrite <- app_comm_cons in H.
+  inversion H.
+  subst.
+  left; left; auto.
+  set (IHa _ _ H0) as H'.
+  destruct H'.
+  left; right; auto.
+  right; auto.
+  Qed.
+
+Lemma distinct_lemma : forall {T} (a b:list T) a0, distinct (app a (a0 :: b)) -> distinct (app a b).
+  intros.
+  induction a; simpl; auto.
+  simpl in H.
+  inversion H; auto.
+  assert (distinct (app a1 b)) as Q.
+  intros.
+  apply IHa.
+  clear IHa.
+  rewrite <- app_comm_cons in H.
+  inversion H; subst; auto.
+  apply distinct_cons; [ idtac | apply Q ].
+  intros.
+  apply in_both in H0.
+  destruct H0.
+  rewrite <- app_comm_cons in H.
+  inversion H; subst; auto.
+  apply H3.
+  apply In_both; auto.
+  rewrite <- app_comm_cons in H.
+  inversion H; subst; auto.
+  apply H3.
+  apply In_both'; auto.
+  simpl.
+  right; auto.
+  Qed.
+
+Lemma nil_app : forall {T}(a:list T) x, x::a = (app (x::nil) a).
+  induction a; intros; simpl; auto.
+  Qed.
+
+Lemma distinct_swap : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
+  intros.
+  induction b.
+  rewrite <- app_nil_end in H; auto.
+  rewrite <- app_comm_cons.
+  set (distinct_lemma _ _ _ H) as H'.
+  set (IHb H') as H''.
+  apply distinct_cons; [ idtac | apply H'' ].
+  intros.
+  apply in_both in H0.
+  clear H'' H'.
+  destruct H0.
+  apply distinct_app in H.
+  destruct H.
+  inversion H1; auto.
+  clear IHb.
+  rewrite nil_app in H.
+  rewrite ass_app in H.
+  apply distinct_app in H.
+  destruct H; auto.
+  apply distinct_swap' in H.
+  inversion H; auto.
+  Qed.
+
+Lemma update_xiv_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
+  forall v1 v2,
+  distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) ->
+  mapOptionTree (update_xi ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) =
+  mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
+  induction varstypes; intros.
+  destruct a; simpl; [ idtac | reflexivity ].
+  destruct p.
+  simpl.
+  simpl in H.
+  induction (leaves v1).
+    simpl; auto.
+    destruct (eqd_dec v v); auto.
+    assert False. apply n. auto. inversion H0.
+    simpl.
+    destruct a.
+      destruct (eqd_dec v0 v); subst; auto.
+      simpl in H.
+      rewrite map_app in H.
+      simpl in H.
+      rewrite nil_app in H.
+      apply distinct_swap in H.
+      rewrite app_ass in H.
+      apply distinct_app in H.
+      destruct H.
+      apply distinct_swap in H0.
+      simpl in H0.
+      inversion H0; subst.
+      assert False.
+      apply H3.
+      simpl; left; auto.
+      inversion H1.
+    apply IHl.
+      simpl in H.
+      inversion H; auto.
+  set (IHvarstypes1 v1 (varstypes2,,v2)) as i1.
+    set (IHvarstypes2 (v1,,varstypes1) v2) as i2.
+    simpl in *.
+    rewrite <- i1.
+    rewrite <- i2.
+    rewrite ass_app. 
+    rewrite ass_app. 
+    rewrite ass_app. 
+    rewrite ass_app. 
+    reflexivity.
+    clear i1 i2 IHvarstypes1 IHvarstypes2.
+    repeat rewrite ass_app in *; auto.
+    clear i1 i2 IHvarstypes1 IHvarstypes2.
+    repeat rewrite ass_app in *; auto.
+    Qed.
+
+Lemma update_xiv_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
+  distinct (map (@fst _ _) (leaves varstypes)) ->
+  mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
+  mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
+  set (update_xiv_lemma' Γ ξ lev varstypes [] []) as q.
+  simpl in q.
+  rewrite <- app_nil_end in q.
+  apply q.
+  Qed.
+
+Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}{l'}(exp:Expr Γ' Δ' ξ' τ' l') : Tree ??VV :=
+  match exp as E in Expr Γ Δ ξ τ l with
+  | EGlobal  Γ Δ ξ _ _ _                          => []
   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
   | ELam     Γ Δ ξ t1 t2 lev v    e               => stripOutVars (v::nil) (expr2antecedent e)
-  | ELet     Γ Δ ξ tv t  lev v ev ebody           => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
+  | ELet     Γ Δ ξ tv t  lev v ev ebody           => (expr2antecedent ev),,((stripOutVars (v::nil) (expr2antecedent ebody)))
   | EEsc     Γ Δ ξ ec t lev e                     => expr2antecedent e
   | EBrak    Γ Δ ξ ec t lev e                     => expr2antecedent e
   | ECast    Γ Δ ξ γ t1 t2 lev      e             => expr2antecedent e
-  | ENote    Γ Δ ξ t n e                          => expr2antecedent e
+  | ENote    Γ Δ ξ t l n e                        => expr2antecedent e
   | ETyLam   Γ Δ ξ κ σ l e                        => expr2antecedent e
   | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => expr2antecedent e
   | ECoApp   Γ Δ κ γ σ₁ σ₂ σ ξ l      e           => expr2antecedent e
   | ETyApp   Γ Δ κ σ τ ξ  l    e                  => expr2antecedent e
-  | ELetRec  Γ Δ ξ l τ vars branches body         =>
+  | ELetRec  Γ Δ ξ l τ vars _ branches body       =>
       let branch_context := eLetRecContext branches
-   in let all_contexts := (expr2antecedent body),,branch_context
+   in let all_contexts := branch_context,,(expr2antecedent body)
    in     stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
   | ECase    Γ Δ ξ l tc tbranches atypes e' alts =>
     ((fix varsfromalts (alts:
-               Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
-                            & Expr (sac_Γ scb Γ)
-                                   (sac_Δ scb Γ atypes (weakCK'' Δ))
-                                   (scbwv_ξ scb ξ l)
-                                   (weakLT' (tbranches@@l)) }
+               Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
+                            & Expr (sac_gamma sac Γ)
+                                   (sac_delta sac Γ atypes (weakCK'' Δ))
+                                   (scbwv_xi scb ξ l)
+                                   (weakT' tbranches) (weakL' l)} }
       ): Tree ??VV :=
       match alts with
         | T_Leaf None     => []
-        | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) (expr2antecedent (projT2 h))
+        | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h)))
         | T_Branch b1 b2  => (varsfromalts b1),,(varsfromalts b2)
       end) alts),,(expr2antecedent e')
 end
 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
 match elrb with
   | ELR_nil    Γ Δ ξ lev  => []
-  | ELR_leaf   Γ Δ ξ lev v e => expr2antecedent e
+  | ELR_leaf   Γ Δ ξ lev v t e => expr2antecedent e
   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
 end.
 
 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
-  (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes
-                            & Expr (sac_Γ scb Γ)
-                                   (sac_Δ scb Γ atypes (weakCK'' Δ))
-                                   (scbwv_ξ scb ξ l)
-                                   (weakLT' (tbranches@@l)) })
-  : ProofCaseBranch tc Γ Δ l tbranches atypes.
+(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
+                            & Expr (sac_gamma sac Γ)
+                                   (sac_delta sac Γ atypes (weakCK'' Δ))
+                                   (scbwv_xi scb ξ l)
+                                   (weakT' tbranches) (weakL' l) } })
+  : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
+  destruct alt.
+  exists x.
   exact
-    {| pcb_scb := projT1 alt
-     ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt)))
+    {| pcb_freevars := mapOptionTree ξ
+      (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
+        (expr2antecedent (projT2 s)))
      |}.
      Defined.
 
-Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) :=
-  match elrb with
-  | ELR_nil    Γ Δ ξ lev  => []
-  | ELR_leaf   Γ Δ ξ  lev  v e => [ξ v]
-  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
-  end.
-
-Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
-  match elrb with
-  | ELR_nil    Γ Δ ξ lev  => []
-  | ELR_leaf   Γ Δ ξ  lev  v e => [v]
-  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
-  end.
 
-Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):=
+Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
   match elrb with
   | ELR_nil    Γ Δ ξ lev  => []
-  | ELR_leaf   Γ Δ ξ  lev  v e => [(v, ξ v)]
-  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
+  | ELR_leaf   Γ Δ ξ  lev  v t e => [t]
+  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
   end.
 
-
 Lemma stripping_nothing_is_inert
   {Γ:TypeEnv}
   (ξ:VV -> LeveledHaskType Γ ★)
@@ -154,58 +584,158 @@ Lemma stripping_nothing_is_inert
     fold stripOutVars.
     simpl.
     fold (stripOutVars nil).
-    rewrite IHtree1.
-    rewrite IHtree2.
+    rewrite <- IHtree1 at 2.
+    rewrite <- IHtree2 at 2.
     reflexivity.
     Qed.
 
+Definition factorContextLeft
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     ctx    (* initial context *)
+     (ξ:VV -> LeveledHaskType Γ ★)
+     :
+ 
+    (* a proof concluding in a context where that variable does not appear *)
+     sum (Arrange
+          (mapOptionTree ξ                        ctx                        )
+          (mapOptionTree ξ ([],,(stripOutVars (v::nil) ctx))                ))
+   
+    (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
+        (Arrange
+          (mapOptionTree ξ                         ctx                       )
+          (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx))                )).
+
+  induction ctx.
+  
+    refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
+  
+        (* nonempty leaf *)
+        destruct case_Some.
+          unfold stripOutVars in *; simpl.
+          unfold dropVar.
+          unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 
+          destruct (eqd_dec v' v); subst.
+          
+            (* where the leaf is v *)
+            apply inr.
+              subst.
+              apply AuCanR.
 
-Definition arrangeContext 
+            (* where the leaf is NOT v *)
+            apply inl.
+              apply AuCanL.
+  
+        (* empty leaf *)
+        destruct case_None.
+          apply inl; simpl in *.
+          apply AuCanR.
+  
+      (* branch *)
+      refine (
+        match IHctx1 with
+          | inr lpf =>
+            match IHctx2 with
+              | inr rpf => let case_Both := tt in _
+              | inl rpf => let case_Left := tt in _
+            end
+          | inl lpf =>
+            match IHctx2 with
+              | inr rpf => let case_Right   := tt in _
+              | inl rpf => let case_Neither := tt in _
+            end
+        end); clear IHctx1; clear IHctx2.
+
+    destruct case_Neither.
+      apply inl.
+      simpl.
+      eapply AComp; [idtac | apply AuCanL ].
+        exact (AComp
+          (* order will not matter because these are central as morphisms *)
+          (ARight _ (AComp lpf (ACanL _)))
+          (ALeft  _ (AComp rpf (ACanL _)))).
+
+    destruct case_Right.
+      apply inr.
+      unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
+      fold (stripOutVars (v::nil)).
+      eapply AComp; [ idtac | eapply pivotContext' ].
+      eapply AComp.
+      eapply ARight.
+      eapply AComp.
+      apply lpf.
+      apply ACanL.
+      eapply ALeft.
+      apply rpf.
+
+    destruct case_Left.
+      apply inr.
+      fold (stripOutVars (v::nil)).
+      simpl.
+      eapply AComp.
+      eapply ALeft.
+      eapply AComp.
+      apply rpf.
+      simpl.
+      eapply ACanL.
+      eapply AComp; [ idtac | eapply AuAssoc ].
+      eapply ARight.
+      apply lpf.
+
+    destruct case_Both.
+      apply inr.
+      simpl.
+      eapply AComp; [ idtac | eapply ARight; eapply ACont ].
+      eapply AComp; [ eapply ARight; eapply lpf | idtac ].
+      eapply AComp; [ eapply ALeft; eapply rpf | idtac ].
+      clear lpf rpf.
+      simpl.
+      apply arrangeSwapMiddle.
+      Defined.
+
+Definition factorContextRight
      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)
      ctx    (* initial context *)
-     τ      (* type of succedent *)
      (ξ:VV -> LeveledHaskType Γ ★)
      :
  
     (* a proof concluding in a context where that variable does not appear *)
-    sum (ND (@URule Γ Δ)
-          [Γ >> Δ > mapOptionTree ξ                        ctx                        |- τ]
-          [Γ >> Δ > mapOptionTree ξ (stripOutVars (v::nil) ctx),,[]                   |- τ])
+     sum (Arrange
+          (mapOptionTree ξ                        ctx                        )
+          (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[]                   ))
    
     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
-        (ND (@URule Γ Δ)
-          [Γ >> Δ > mapOptionTree ξ                         ctx                       |- τ]
-          [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])                |- τ]).
+        (Arrange
+          (mapOptionTree ξ                         ctx                       )
+          (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])                )).
 
-  induction ctx; simpl in *.
+  induction ctx.
   
-    refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end); simpl in *.
+    refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
   
         (* nonempty leaf *)
         destruct case_Some.
           unfold stripOutVars in *; simpl.
           unfold dropVar.
           unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
-          destruct (eqd_dec v v'); simpl in *.
 
+          destruct (eqd_dec v' v); subst.
+          
             (* where the leaf is v *)
             apply inr.
               subst.
-              apply nd_rule.
-              apply RuCanL.
+              apply AuCanL.
 
             (* where the leaf is NOT v *)
             apply inl.
-              apply nd_rule.
-              apply RuCanR.
+              apply AuCanR.
   
         (* empty leaf *)
         destruct case_None.
           apply inl; simpl in *.
-          apply nd_rule.
-          apply RuCanR.
+          apply AuCanR.
   
       (* branch *)
       refine (
@@ -224,94 +754,159 @@ Definition arrangeContext
 
     destruct case_Neither.
       apply inl.
-      eapply nd_comp; [idtac | eapply nd_rule; apply RuCanR ].
-        exact (nd_comp
+      eapply AComp; [idtac | apply AuCanR ].
+        exact (AComp
           (* order will not matter because these are central as morphisms *)
-          (ext_right _ _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _))))
-          (ext_left  _ _ _ (nd_comp rpf (nd_rule (@RCanR _ _ _ _))))).
+          (ARight _ (AComp lpf (ACanR _)))
+          (ALeft  _ (AComp rpf (ACanR _)))).
 
 
     destruct case_Right.
       apply inr.
       fold (stripOutVars (v::nil)).
-      set (ext_right (mapOptionTree ξ ctx2) _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) as q.
+      set (ARight (mapOptionTree ξ ctx2)  (AComp lpf ((ACanR _)))) as q.
       simpl in *.
-      eapply nd_comp.
+      eapply AComp.
       apply q.
       clear q.
       clear lpf.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
-      eapply nd_comp; [ idtac | eapply nd_rule; apply RAssoc ].
-      set (ext_left (mapOptionTree ξ (stripOutVars (v :: nil) ctx1)) [Γ >> Δ>mapOptionTree ξ ctx2 |- τ]
-                                                            [Γ >> Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx2),,[ξ v])  |- τ]) as qq.
-      apply qq.
-      clear qq.
+      eapply AComp; [ idtac | apply AAssoc ].
+      apply ALeft.
       apply rpf.
 
     destruct case_Left.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).
-      eapply nd_comp; [ idtac | eapply pivotContext ].
-      set (nd_comp rpf (nd_rule (@RCanR _ _ _ _ ) ) ) as rpf'.
-      set (ext_left ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) _ _ rpf') as qq.
+      eapply AComp; [ idtac | eapply pivotContext ].
+      set (AComp rpf (ACanR _ )) as rpf'.
+      set (ALeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
       simpl in *.
-      eapply nd_comp; [ idtac | apply qq ].
+      eapply AComp; [ idtac | apply qq ].
       clear qq rpf' rpf.
-      set (ext_right (mapOptionTree ξ ctx2) [Γ >>Δ> mapOptionTree ξ ctx1 |- τ] [Γ >>Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v]) |- τ]) as q.
-      apply q.
-      clear q.
+      apply (ARight (mapOptionTree ξ ctx2)).
       apply lpf.
 
     destruct case_Both.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).
-      eapply nd_comp; [ idtac | eapply copyAndPivotContext ].
-        exact (nd_comp
-          (* order will not matter because these are central as morphisms *)
-          (ext_right _ _ _ lpf)
-          (ext_left  _ _ _ rpf)).
+      eapply AComp; [ idtac | eapply copyAndPivotContext ].
+        (* order will not matter because these are central as morphisms *)
+        exact (AComp (ARight _ lpf) (ALeft _ rpf)).
 
     Defined.
 
-(* same as before, but use RWeak if necessary *)
-Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ : 
-       ND (@URule Γ Δ)
-          [Γ >> Δ>mapOptionTree ξ                        ctx                |- τ]
-          [Γ >> Δ>mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        |- τ].
-  set (arrangeContext Γ Δ v ctx τ ξ) as q.
+(* same as before, but use AWeak if necessary *)
+Definition factorContextLeftAndWeaken  
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     ctx    (* initial context *)
+     (ξ:VV -> LeveledHaskType Γ ★) :
+       Arrange
+          (mapOptionTree ξ                        ctx                )
+          (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx))        ).
+  set (factorContextLeft Γ Δ v ctx ξ) as q.
   destruct q; auto.
-  eapply nd_comp; [ apply n | idtac ].
-  clear n.
-  refine (ext_left _ _ _ (nd_rule (RWeak _ _))).
+  eapply AComp; [ apply a | idtac ].
+  refine (ARight _ (AWeak _)).
   Defined.
 
-Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, 
-  ND (@URule Γ Δ)
-    [Γ >> Δ>(mapOptionTree ξ ctx)                                       |-  z]
-    [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |-  z].
+Definition factorContextLeftAndWeaken''
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
+  distinct (leaves v) ->
+  Arrange
+    ((mapOptionTree ξ ctx)                                       )
+    ((mapOptionTree ξ v),,(mapOptionTree ξ (stripOutVars (leaves v) ctx))).
 
-  induction v.
+  induction v; intros.
     destruct a.
     unfold mapOptionTree in *.
     simpl in *.
     fold (mapOptionTree ξ) in *.
     intros.
-    apply arrangeContextAndWeaken.
+    set (@factorContextLeftAndWeaken) as q.
+    simpl in q.
+    apply q.
+    apply Δ.
 
   unfold mapOptionTree; simpl in *.
     intros.
     rewrite (@stripping_nothing_is_inert Γ); auto.
-    apply nd_rule.
-    apply RuCanR.
+    apply AuCanL.
     intros.
     unfold mapOptionTree in *.
     simpl in *.
     fold (mapOptionTree ξ) in *.
     set (mapOptionTree ξ) as X in *.
 
-    set (IHv2 ((stripOutVars (leaves v1) ctx),, v1) z) as IHv2'.
+    set (distinct_app _ _ _ H) as H'.
+    destruct H' as [H1 H2].
+
+    set (IHv1 (v2,,(stripOutVars (leaves v2) ctx))) as IHv1'.
+
+    unfold X in *.
+    simpl in *.
+      rewrite <- strip_twice_lemma.
+      set (notin_strip_inert' v2 (leaves v1)) as q.
+      unfold stripOutVars in q.
+      rewrite q in IHv1'.
+      clear q.
+    eapply AComp; [ idtac | eapply AAssoc ].
+    eapply AComp; [ idtac | eapply IHv1' ].
+    clear IHv1'.
+    apply IHv2; auto.
+    auto.
+    auto.
+    Defined.
+
+(* same as before, but use AWeak if necessary *)
+Definition factorContextRightAndWeaken  
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     ctx    (* initial context *)
+     (ξ:VV -> LeveledHaskType Γ ★) :
+       Arrange
+          (mapOptionTree ξ                        ctx                )
+          (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        ).
+  set (factorContextRight Γ Δ v ctx ξ) as q.
+  destruct q; auto.
+  eapply AComp; [ apply a | idtac ].
+  refine (ALeft _ (AWeak _)).
+  Defined.
+
+Definition factorContextRightAndWeaken''
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
+  distinct (leaves v) ->
+  Arrange
+    ((mapOptionTree ξ ctx)                                       )
+    ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).
+
+  induction v; intros.
+    destruct a.
+    unfold mapOptionTree in *.
+    simpl in *.
+    fold (mapOptionTree ξ) in *.
+    intros.
+    apply factorContextRightAndWeaken.
+    apply Δ.
+
+  unfold mapOptionTree; simpl in *.
+    intros.
+    rewrite (@stripping_nothing_is_inert Γ); auto.
+    apply AuCanR.
+    intros.
+    unfold mapOptionTree in *.
+    simpl in *.
+    fold (mapOptionTree ξ) in *.
+    set (mapOptionTree ξ) as X in *.
+
+    set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.
     unfold stripOutVars in IHv2'.
     simpl in IHv2'.
     fold (stripOutVars (leaves v2)) in IHv2'.
@@ -321,315 +916,240 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
     simpl in IHv2'.
     fold (mapOptionTree ξ) in IHv2'.
     fold X in IHv2'.
-    set (nd_comp (IHv1 _ _) IHv2') as qq.
-    eapply nd_comp.
+    set (distinct_app _ _ _ H) as H'.
+    destruct H' as [H1 H2].
+    set (AComp (IHv1 _ H1) (IHv2' H2)) as qq.
+    eapply AComp.
       apply qq.
       clear qq IHv2' IHv2 IHv1.
-        
-      assert ((stripOutVars (leaves v2) (stripOutVars (leaves v1) ctx))=(stripOutVars (app (leaves v1) (leaves v2)) ctx)).
-        admit.
-        rewrite H.
-        clear H.
-
-      (* FIXME: this only works because the variables are all distinct, but I need to prove that *)
-      assert ((stripOutVars (leaves v2) v1) = v1).
-        admit.
-        rewrite H.
-        clear H.
-
-        apply nd_rule.
-        apply RCossa.
+      rewrite strip_swap_lemma.
+      rewrite strip_twice_lemma.
+      rewrite (notin_strip_inert' v1 (leaves v2)).
+        apply AuAssoc.
+        apply distinct_swap.
+        auto.
     Defined.
 
-Definition update_ξ'' {Γ} ξ tree lev :=
-(update_ξ ξ
-                  (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@  lev ⟩)
-                     (leaves tree))).
-
-Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree lev :
-      mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree)
+Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
+      mapOptionTree (update_xi ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
     = mapOptionTree ξ (stripOutVars (v :: nil) tree).
-  induction tree; simpl in *; try reflexivity; auto.
-
-  unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ ((v,lev)::nil))) in *.
-  destruct a; simpl; try reflexivity.
-  unfold update_ξ.
-  simpl.
-  unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
-  unfold update_ξ.
-  unfold dropVar.
+  set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
+  rewrite p.
   simpl.
-  set (eqd_dec v v0) as q.
-  assert (q=eqd_dec v v0).
-    reflexivity.
-  destruct q.
-  reflexivity.
-  rewrite <- H.
-  reflexivity.
-  auto.
-  unfold mapOptionTree.
-  unfold mapOptionTree in IHtree1.
-  unfold mapOptionTree in IHtree2.
-  simpl in *.
-  simpl in IHtree1.
-  fold (stripOutVars (v::nil)).
-  rewrite <- IHtree1.
-  rewrite <- IHtree2.
   reflexivity.
   Qed.
 
-
-
-Lemma updating_stripped_tree_is_inert'
-  {Γ} lev
-  (ξ:VV -> LeveledHaskType Γ ★)
-  tree tree2 :
-    mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2)
-  = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2).
-admit.
-  Qed.
-
-Lemma updating_stripped_tree_is_inert''
-  {Γ}
-  (ξ:VV -> LeveledHaskType Γ ★)
-  v tree lev :
-    mapOptionTree   (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree)
-  = mapOptionTree ξ (stripOutVars  (map (@fst _ _) v) tree).
-admit.
-  Qed.
-
-(*
-Lemma updating_stripped_tree_is_inert'''
-  {Γ}
-  (ξ:VV -> LeveledHaskType Γ)
-{T}
-  (idx:Tree ??T) (types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx) tree
-:
-    mapOptionTree   (update_ξ''' ξ types vars) (stripOutVars (leaves (unshape vars)) tree)
-  = mapOptionTree ξ (stripOutVars (leaves (unshape vars)) tree).
-admit.
-  Qed.
-*)
-
-(* IDEA: use multi-conclusion proofs instead *)
+(* TODO: use multi-conclusion proofs instead *)
 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := 
   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
-  | lrsp_leaf : forall v  e,
-    (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) ->
-    LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ e)
+  | lrsp_leaf : forall v t e ,
+    (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t]@lev]) ->
+    LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
   | lrsp_cons : forall t1 t2 b1 b2,
     LetRecSubproofs Γ Δ ξ lev t1 b1 ->
     LetRecSubproofs Γ Δ ξ lev t2 b2 ->
     LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
 
-Lemma cheat1 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
-  eLetRecTypes branches =
-    mapOptionTree  (update_ξ'' ξ tree lev)
-    (mapOptionTree (@fst _ _) tree).
-  intros.
-  induction branches.
-  reflexivity.
-  simpl.
-  unfold update_ξ.
-  unfold mapOptionTree; simpl.
-admit.
-admit.
-  Qed.
-Lemma cheat2 : forall Γ Δ ξ l tc tbranches atypes e alts',
-mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
-= 
-(*
-((mapOptionTreeAndFlatten
-(fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h)))
-                  (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)).
-*)
-((mapOptionTreeAndFlatten pcb_freevars
-           (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ  (expr2antecedent e)).
-admit.
-Qed.
-Lemma cheat3 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
-  admit.
-  Qed.
-Lemma cheat4 : forall {A}(t:list A), leaves (unleaves t) = t.
-admit.
-Qed.
-
-Lemma letRecSubproofsToND Γ Δ ξ lev tree branches
-    : LetRecSubproofs Γ Δ ξ lev tree branches ->
-    ND Rule []
-    [ Γ > Δ >
-      mapOptionTree ξ (eLetRecContext branches)
-      |-
-  eLetRecTypes branches
-    ].
-  intro X.
-  induction X; intros; simpl in *.
+Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
+  LetRecSubproofs Γ Δ ξ lev tree branches ->
+    ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
+      |- (mapOptionTree (@snd _ _) tree) @ lev ].
+  intro X; induction X; intros; simpl in *.
     apply nd_rule.
-      apply REmptyGroup.
+      apply RVoid.
     set (ξ v) as q in *.
       destruct q.
       simpl in *.
-      assert (h0=lev).
-        admit.
-        rewrite H.
       apply n.
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
-    eapply nd_comp; [ apply nd_llecnac | idtac ].
-    apply nd_prod; auto.
-  Defined.
-
-
-Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev,
-  mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z.
-admit.
-  Qed.
-
-
+    eapply nd_comp; [ idtac | eapply RCut' ].
+      eapply nd_comp; [ apply nd_llecnac | idtac ].
+      apply nd_prod.
+      apply IHX1.
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ].
+      apply IHX2.
+      Defined.
 
 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
-    forall branches body,
-    ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] -> 
-    LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches ->
-    ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
+    forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),
+    ND Rule [] [Γ > Δ > mapOptionTree (update_xi ξ lev (leaves tree)) (expr2antecedent body) |- [τ ]@ lev] -> 
+    LetRecSubproofs Γ Δ (update_xi ξ lev (leaves tree)) lev tree branches ->
+    ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ ]@ lev].
 
   (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
-  simpl.
   intro branches.
   intro body.
+  intro disti.
   intro pf.
   intro lrsp.
-  set ((update_ξ ξ
-           (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@  lev ⟩)
-              (leaves tree)))) as ξ' in *.
+
+  assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'.
+    apply disti.
+    rewrite mapleaves in disti'.
+
+  set (@update_xiv_lemma _ Γ ξ lev tree disti') as ξlemma.
+    rewrite <- mapOptionTree_compose in ξlemma.
+
+  set ((update_xi ξ lev (leaves tree))) as ξ' in *.
   set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
   set (mapOptionTree (@fst _ _) tree) as pctx.
   set (mapOptionTree ξ' pctx) as passback.
-  set (fun a b => @RLetRec Γ Δ a b passback) as z.
+  set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
   clear z.
 
-  set (@arrangeContextAndWeaken''  Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
+  set (@factorContextRightAndWeaken''  Γ Δ  pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
   unfold passback in *; clear passback.
   unfold pctx in *; clear pctx.
-  eapply UND_to_ND in q'.
+  set (q' disti) as q''.
 
   unfold ξ' in *.
-  set (@updating_stripped_tree_is_inert') as zz.
-  unfold update_ξ'' in *.
-  rewrite zz in q'.
+  set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
+  rewrite <- mapleaves in zz.
+  rewrite zz in q''.
   clear zz.
   clear ξ'.
-  simpl in q'.
-
-  eapply nd_comp; [ idtac | apply q' ].
+  Opaque stripOutVars.
+  simpl.
+  rewrite <- mapOptionTree_compose in q''.
+  rewrite <- ξlemma.
+  eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ _ q'') ].
   clear q'.
-  unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)).
-
+  clear q''.
   simpl.
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
 
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
-    eapply nd_comp; [ apply nd_llecnac | idtac ].
-    apply nd_prod; auto.
-    rewrite cheat1 in q.
-    set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz.
-    unfold update_ξ'' in *.
-    rewrite <- zz in q.
-    apply q.
-  Defined.
-
-
-Lemma updating_stripped_tree_is_inert''' : forall Γ tc ξ l t atypes x,
-         mapOptionTree (scbwv_ξ(Γ:=Γ)(tc:=tc)(atypes:=atypes) x ξ l)
-           (stripOutVars (vec2list (scbwv_exprvars x)) t)
-             =
-         mapOptionTree (weakLT' ○ ξ)
-           (stripOutVars (vec2list (scbwv_exprvars x)) t).
-  admit.
+    eapply nd_comp; [ idtac | eapply RCut' ].
+      eapply nd_comp; [ apply nd_llecnac | idtac ].
+      apply nd_prod.
+      apply q.
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ].
+      apply pf.
+      Defined.
+
+Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
+  forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
+    forall l ξ,
+      vec2list (vec_map (scbwv_xi scb ξ l) (scbwv_exprvars scb)) =
+      vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
+  intros.
+  unfold scbwv_xi.
+  unfold scbwv_varstypes.
+  set (@update_xiv_lemma _ _ (weakLT' ○ ξ) (weakL' l)
+    (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
+    ) as q.
+  rewrite <- mapleaves' in q.
+  rewrite <- mapleaves' in q.
+  rewrite <- mapleaves' in q.
+  rewrite <- mapleaves' in q.
+  set (fun z => unleaves_injective _ _ _ (q z)) as q'.
+  rewrite vec2list_map_list2vec in q'.
+  rewrite fst_zip in q'.
+  rewrite vec2list_map_list2vec in q'.
+  rewrite vec2list_map_list2vec in q'.
+  rewrite snd_zip in q'.
+  rewrite leaves_unleaves in q'.
+  rewrite vec2list_map_list2vec in q'.
+  rewrite vec2list_map_list2vec in q'.
+  apply q'.
+  rewrite fst_zip.
+  apply scbwv_exprvars_distinct.
   Qed.
 
 
-Lemma updating_stripped_tree_is_inert'''' : forall Γ Δ ξ l tc atypes tbranches 
-(x:StrongCaseBranchWithVVs(Γ:=Γ) VV eqd_vv tc atypes)
-(e0:Expr (sac_Γ x Γ) (sac_Δ x Γ atypes (weakCK'' Δ)) 
-    (scbwv_ξ x ξ l) (weakT' tbranches @@  weakL' l)) ,
-mapOptionTree (weakLT' ○ ξ)
-        (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
-unleaves (vec2list (sac_types x Γ atypes)) @@@ weakL' l
-=
-mapOptionTree (weakLT' ○ ξ)
-        (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
-         mapOptionTree
-           (update_ξ (weakLT' ○ ξ)
-              (vec2list
-                 (vec_map
-                    (fun
-                       x0 : VV *
-                            HaskType
-                              (app (vec2list (sac_ekinds x)) Γ)
-                              ★ => ⟨fst x0, snd x0 @@  weakL' l ⟩)
-                    (vec_zip (scbwv_exprvars x)
-                       (sac_types x Γ atypes)))))
-           (unleaves (vec2list (scbwv_exprvars x)))
-.
-admit.
-Qed.
-
-
+Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
+   (alts':Tree
+            ??{sac : StrongAltCon &
+              {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
+              Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ))
+                (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}),
 
+      (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
+        (mapOptionTree mkProofCaseBranch alts'))
+    ,,
+    mapOptionTree ξ  (expr2antecedent e) =
+  mapOptionTree ξ
+        (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
+  intros.
+  simpl.
+  Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
+  hack.
+  induction alts'.
+  destruct a; simpl.
+  destruct s; simpl.
+  unfold mkProofCaseBranch.
+  reflexivity.
+  reflexivity.
+  simpl.
+  rewrite IHalts'1.
+  rewrite IHalts'2.
+  reflexivity.
+  rewrite H.
+  reflexivity.
+  Qed.
 
 Definition expr2proof  :
-  forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
-    ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
+  forall Γ Δ ξ τ l (e:Expr Γ Δ ξ τ l),
+    ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ] @ l].
 
-  refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
-    : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
-    match exp as E in Expr Γ Δ ξ τ with
+  refine (fix expr2proof Γ' Δ' ξ' τ' l' (exp:Expr Γ' Δ' ξ' τ' l') {struct exp}
+    : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ'] @ l'] :=
+    match exp as E in Expr Γ Δ ξ τ l with
+    | EGlobal  Γ Δ ξ     g v lev                    => let case_EGlobal := tt in _
     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in 
-                                                        (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
-    | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+                                                        (fun e1' e2' => _) (expr2proof _ _ _ _ _ e1) (expr2proof _ _ _ _ _ e2)
+    | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ELet     Γ Δ ξ tv t      v lev ev ebody       => let case_ELet := tt in 
-                                                       (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody) 
-    | ELetRec  Γ Δ ξ lev t tree branches ebody      =>
-      let ξ' := update_ξ'' ξ tree lev in
-      let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) 
-((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
+                                                       (fun pf_let pf_body => _) (expr2proof _ _ _ _ _ ev) (expr2proof _ _ _ _ _ ebody) 
+    | ELetRec  Γ Δ ξ lev t tree disti branches ebody =>
+      let ξ' := update_xi ξ lev (leaves tree) in
+      let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ _ ebody) 
+        ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
         (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
         : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
         match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
           | ELR_nil    Γ Δ ξ lev  => lrsp_nil _ _ _ _
-          | ELR_leaf   Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
+          | ELR_leaf   Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ _ e)
           | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
         end
         ) _ _ _ _ tree branches)
-    | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in (fun e' => _) (expr2proof _ _ _ _ e)
-    | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
-    | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
-    | ENote    Γ Δ ξ t n e                          => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
-    | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
-    | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
-    | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
-    | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+    | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+    | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+    | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+    | ENote    Γ Δ ξ t _ n e                        => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+    | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+    | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+    | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+    | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ECase    Γ Δ ξ l tc tbranches atypes e alts' => 
       let dcsp :=
         ((fix mkdcsp (alts:
-               Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
-                            & Expr (sac_Γ scb Γ)
-                                   (sac_Δ scb Γ atypes (weakCK'' Δ))
-                                   (scbwv_ξ scb ξ l)
-                                   (weakLT' (tbranches@@l)) })
-          : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
-        match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
-          | T_Leaf None       => let case_nil := tt in _
-          | T_Leaf (Some x)   => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
+               Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
+                            & Expr (sac_gamma sac Γ)
+                                   (sac_delta sac Γ atypes (weakCK'' Δ))
+                                   (scbwv_xi scb ξ l)
+                                   (weakT' tbranches) (weakL' l) } })
+          : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
+        match alts as ALTS return ND Rule [] 
+          (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
+          | T_Leaf None      => let case_nil := tt in _
           | T_Branch b1 b2   => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
+          | T_Leaf (Some x)  =>
+            match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
+            existT sac (existT scbx ex) =>
+            (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ _ ex)
+        end
         end) alts')
-        in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+        in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     end
-); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
+  ); clear exp ξ' τ' Γ' Δ' l' expr2proof; try clear mkdcsp.
+
+    destruct case_EGlobal.
+      apply nd_rule.
+      simpl.
+      apply (RGlobal _ _ _  g).
 
     destruct case_EVar.
       apply nd_rule.
@@ -643,25 +1163,24 @@ Definition expr2proof  :
 
     destruct case_EApp.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
-      eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
+      eapply nd_comp; [ idtac
+        | eapply nd_rule;
+          apply (@RApp _ _ _ _ t2 t1) ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod; auto.
-      apply e1'.
-      apply e2'.
 
     destruct case_ELam; intros.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
-      set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'.
-      set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
-        apply UND_to_ND in pfx.
-        unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
+      set (update_xi ξ lev ((v,t1)::nil)) as ξ'.
+      set (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
+        eapply RArrange in pfx.
+        unfold mapOptionTree in pfx; simpl in pfx.
         unfold ξ' in pfx.
-        fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx.
         rewrite updating_stripped_tree_is_inert in pfx.
-        unfold update_ξ in pfx.
+        unfold update_xi in pfx.
         destruct (eqd_dec v v).
-        eapply nd_comp; [ idtac | apply pfx ].
+        eapply nd_comp; [ idtac | apply (nd_rule pfx) ].
         clear pfx.
         apply e'.
         assert False.
@@ -670,25 +1189,24 @@ Definition expr2proof  :
         inversion H.
 
     destruct case_ELet; intros; simpl in *.
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
-      eapply nd_comp; [ apply nd_llecnac | idtac ].
-      apply nd_prod; [ idtac | apply pf_let].
-      clear pf_let.
+      eapply nd_comp; [ idtac | eapply RLet ].
+      eapply nd_comp; [ apply nd_rlecnac | idtac ].
+      apply nd_prod.
+      apply pf_let.
       eapply nd_comp; [ apply pf_body | idtac ].
-      clear pf_body.
       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).
-      set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
-      set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
+      set (update_xi ξ v ((lev,tv)::nil)) as ξ'.
+      set (factorContextLeftAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
       unfold ξ' in n.
       rewrite updating_stripped_tree_is_inert in n.
-      unfold update_ξ in n.
+      unfold update_xi in n.
       destruct (eqd_dec lev lev).
       unfold ξ'.
-      unfold update_ξ.
-      apply UND_to_ND in n.
-      apply n.
+      unfold update_xi.
+      eapply RArrange in n.
+      apply (nd_rule n).
       assert False. apply n0; auto. inversion H.
 
     destruct case_EEsc.
@@ -731,28 +1249,39 @@ Definition expr2proof  :
       apply e'.
 
     destruct case_leaf.
-      unfold pcb_judg.
+      clear o x alts alts' e.
+      eapply nd_comp; [ apply e' | idtac ].
+      clear e'.
+      apply nd_rule.
+      apply RArrange.
       simpl.
-      repeat rewrite <- mapOptionTree_compose in *.
-      set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
-        (unleaves (vec2list (scbwv_exprvars (projT1 x))))
-      (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
-        _ _
-      ))) as q.
-      rewrite cheat4 in q.
-      rewrite cheat3.
-      unfold weakCK'' in q.
-      simpl in q.
-      rewrite (updating_stripped_tree_is_inert''' Γ tc ξ l _ atypes  (projT1 x)) in q.
-      Ltac cheater Q :=
-       match goal with
-        [ Q:?Y |- ?Z ] =>
-         assert (Y=Z) end.
-      cheater q.
-      admit.
-      rewrite <- H.
-      clear H.
+      rewrite mapleaves'.
+      simpl.
+      rewrite <- mapOptionTree_compose.
+      unfold scbwv_xi.
+      rewrite <- mapleaves'.
+      rewrite vec2list_map_list2vec.
+      unfold sac_gamma.      
+      rewrite <- (scbwv_coherent scbx l ξ).
+      rewrite <- vec2list_map_list2vec.
+      rewrite mapleaves'.
+      set (@factorContextRightAndWeaken'') as q.
+      unfold scbwv_xi.
+      set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
+      unfold scbwv_varstypes in z.
+      rewrite vec2list_map_list2vec in z.
+      rewrite fst_zip in z.
+      rewrite <- z.
+      clear z.
+
+      replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
+        (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
       apply q.
+      apply (sac_delta sac Γ atypes (weakCK'' Δ)).
+      rewrite leaves_unleaves.
+      apply (scbwv_exprvars_distinct scbx).
+      rewrite leaves_unleaves.
+      reflexivity.
 
     destruct case_nil.
       apply nd_id0.
@@ -764,18 +1293,20 @@ Definition expr2proof  :
       apply b2'.
 
     destruct case_ECase.
-      rewrite cheat2.
+    set (@RCase Γ Δ l tc) as q.
+      rewrite <- case_lemma.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
       rewrite <- mapOptionTree_compose.
       apply dcsp.
       apply e'.
 
-    destruct case_ELetRec; simpl in *; intros.
-      set (@letRecSubproofsToND') as q.
-      simpl in q.
-      apply q.
-      clear q.
+    destruct case_ELetRec; intros.
+      unfold ξ'0 in *.
+      clear ξ'0.
+      unfold ξ'1 in *.
+      clear ξ'1.
+      apply letRecSubproofsToND'.
       apply e'.
       apply subproofs.
 
@@ -783,16 +1314,3 @@ Definition expr2proof  :
 
 End HaskStrongToProof.
 
-(*
-
-(* Figure 7, production "decl"; actually not used in this formalization *)
-Inductive Decl :=.
-| DeclDataType     : forall tc:TyCon,      (forall dc:DataCon tc, DataConDecl dc)      -> Decl
-| DeclTypeFunction : forall n t l,         TypeFunctionDecl n t l                      -> Decl
-| DeclAxiom        : forall n ccon vk TV,  @AxiomDecl        n ccon vk  TV             -> Decl.
-
-(* Figure 1, production "pgm" *)
-Inductive Pgm Γ Δ :=
-  mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.
-*)
-