add support for flattening recursive-let

[coq-hetmet.git] / src / HaskStrongToProof.v

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index d17dd38..114f2d9 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -6,6 +6,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
 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 Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.

@@ -15,87 +16,529 @@ Require Import HaskStrong.
 Require Import HaskProof.
 
 Section HaskStrongToProof.
 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 *.
     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 *)
-  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.
-  (* 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.

 
 

-Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
-  match exp as E in Expr Γ Δ ξ τ with
-  | EGlobal  Γ Δ ξ _ _                            => []
+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.
+
+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)
   | 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
   | 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
   | 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
       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:
    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     => []
       ): 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
         | T_Branch b1 b2  => (varsfromalts b1),,(varsfromalts b2)
       end) alts),,(expr2antecedent e')
 end

@@ -107,15 +550,18 @@ match elrb with
 end.
 
 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
 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
   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.
 
      |}.
      Defined.
 

@@ -126,21 +572,6 @@ Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ
   | ELR_leaf   Γ Δ ξ  lev  v t e => [t]
   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
   end.
   | ELR_leaf   Γ Δ ξ  lev  v t e => [t]
   | 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 * HaskType Γ ★):=
-  match elrb with
-  | ELR_nil    Γ Δ ξ lev  => []
-  | ELR_leaf   Γ Δ ξ  lev  v t _ e => [(v, t)]
-  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
-  end.
-*)

 
 Lemma stripping_nothing_is_inert
   {Γ:TypeEnv}
 
 Lemma stripping_nothing_is_inert
   {Γ:TypeEnv}

@@ -158,27 +589,127 @@ Lemma stripping_nothing_is_inert
     reflexivity.
     Qed.
 
     reflexivity.
     Qed.
 

-Ltac eqd_dec_refl X :=
-  destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
-    [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
+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.
+
+            (* 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 arrangeContext 
+Definition factorContextRight

      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)
      ctx    (* initial context *)
      (Γ: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 *)
      (ξ: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 *)
    
     (* 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.
   
 
   induction ctx.
   

@@ -195,19 +726,16 @@ Definition arrangeContext
             (* where the leaf is v *)
             apply inr.
               subst.
             (* where the leaf is v *)
             apply inr.
               subst.

-              apply nd_rule.
-              apply RuCanL.
+              apply AuCanL.

 
             (* where the leaf is NOT v *)
             apply inl.
 
             (* where the leaf is NOT v *)
             apply inl.

-              apply nd_rule.
-              apply RuCanR.
+              apply AuCanR.

   
         (* empty leaf *)
         destruct case_None.
           apply inl; simpl in *.
   
         (* empty leaf *)
         destruct case_None.
           apply inl; simpl in *.

-          apply nd_rule.
-          apply RuCanR.
+          apply AuCanR.

   
       (* branch *)
       refine (
   
       (* branch *)
       refine (

@@ -226,112 +754,138 @@ Definition arrangeContext
 
     destruct case_Neither.
       apply inl.
 
     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 *)
           (* 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)).
 
 
     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 *.
       simpl in *.

-      eapply nd_comp.
+      eapply AComp.

       apply q.
       clear q.
       clear lpf.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       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)).
       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 *.
       simpl in *.

-      eapply nd_comp; [ idtac | apply qq ].
+      eapply AComp; [ idtac | apply qq ].

       clear qq rpf' rpf.
       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)).
       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.
 
 
     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.
   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.
 
   Defined.
 

-Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t).
-  unfold stripOutVars.
-  rewrite <- mapTree_compose.
-  induction t; try destruct a0.
-  simpl.
-  induction x.
-    reflexivity.
-    admit.
-  subst.
-  reflexivity.
-  simpl in *.
-  rewrite <- IHt1.
-  rewrite <- IHt2.
-  reflexivity.
-  Qed.
+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))).

 
 

-Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t.
-  induction x.
-  simpl.
-  admit.
-  rewrite strip_lemma.
-  rewrite IHx.
-  rewrite <- strip_lemma.
-  admit.
-  Qed.
+  induction v; intros.
+    destruct a.
+    unfold mapOptionTree in *.
+    simpl in *.
+    fold (mapOptionTree ξ) in *.
+    intros.
+    set (@factorContextLeftAndWeaken) as q.
+    simpl in q.
+    apply q.
+    apply Δ.

 
 

-Lemma distinct_app1 : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1.
-  admit.
-  Qed.
+  unfold mapOptionTree; simpl in *.
+    intros.
+    rewrite (@stripping_nothing_is_inert Γ); auto.
+    apply AuCanL.
+    intros.
+    unfold mapOptionTree in *.
+    simpl in *.
+    fold (mapOptionTree ξ) in *.
+    set (mapOptionTree ξ) as X in *.

 
 

-Lemma distinct_app2 : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l2.
-  admit.
-  Qed.
+    set (distinct_app _ _ _ H) as H'.
+    destruct H' as [H1 H2].

 
 

-Lemma strip_distinct x y : distinct (app (leaves y) x) -> stripOutVars x y = y.
-  admit.
-  Qed.
+    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.

 
 

-Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, 
+(* 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) ->
   distinct (leaves v) ->

-  ND (@URule Γ Δ)
-    [Γ >> Δ>(mapOptionTree ξ ctx)                                       |-  z]
-    [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |-  z].
+  Arrange
+    ((mapOptionTree ξ ctx)                                       )
+    ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).

 
   induction v; intros.
     destruct a.
 
   induction v; intros.
     destruct a.

@@ -339,20 +893,20 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
     simpl in *.
     fold (mapOptionTree ξ) in *.
     intros.
     simpl in *.
     fold (mapOptionTree ξ) in *.
     intros.

-    apply arrangeContextAndWeaken.
+    apply factorContextRightAndWeaken.
+    apply Δ.

 
   unfold mapOptionTree; simpl in *.
     intros.
     rewrite (@stripping_nothing_is_inert Γ); auto.
 
   unfold mapOptionTree; simpl in *.
     intros.
     rewrite (@stripping_nothing_is_inert Γ); auto.

-    apply nd_rule.
-    apply RuCanR.
+    apply AuCanR.

     intros.
     unfold mapOptionTree in *.
     simpl in *.
     fold (mapOptionTree ξ) in *.
     set (mapOptionTree ξ) as X in *.
 
     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 (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.

     unfold stripOutVars in IHv2'.
     simpl in IHv2'.
     fold (stripOutVars (leaves v2)) in IHv2'.
     unfold stripOutVars in IHv2'.
     simpl in IHv2'.
     fold (stripOutVars (leaves v2)) in IHv2'.

@@ -362,82 +916,34 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
     simpl in IHv2'.
     fold (mapOptionTree ξ) in IHv2'.
     fold X in IHv2'.
     simpl in IHv2'.
     fold (mapOptionTree ξ) in IHv2'.
     fold X in IHv2'.

-    set (nd_comp (IHv1 _ _ (distinct_app1 _ _ _ H)) (IHv2' (distinct_app2 _ _ _ H))) 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.
       apply qq.
       clear qq IHv2' IHv2 IHv1.

+      rewrite strip_swap_lemma.

       rewrite strip_twice_lemma.
       rewrite strip_twice_lemma.

-
-      rewrite (strip_distinct (leaves v2) v1).
-        apply nd_rule.
-        apply RCossa.
+      rewrite (notin_strip_inert' v1 (leaves v2)).
+        apply AuAssoc.
+        apply distinct_swap.

         auto.
     Defined.
 
 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
         auto.
     Defined.
 
 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :

-      mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
+      mapOptionTree (update_xi ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)

     = mapOptionTree ξ (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_ξ ξ lev ((v,t)::nil))) in *.
-  destruct a; simpl; try reflexivity.
-  unfold update_ξ.
+  set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
+  rewrite p.

   simpl.
   simpl.

-  unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
-  unfold update_ξ.
-  unfold dropVar.
-  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.
   reflexivity.

-*)
-admit.
-admit.
-admit.

   Qed.
 
   Qed.
 

-
-Lemma updating_stripped_tree_is_inert'
-  {Γ} lev
-  (ξ:VV -> LeveledHaskType Γ ★)
-  tree tree2 :
-    mapOptionTree (update_ξ ξ lev (leaves tree)) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2)
-  = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2).
-  admit.
-  Qed.
-
-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).
-  intros.
-  unfold scbwv_ξ.
-  unfold scbwv_varstypes.
-  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 t e ,
 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := 
   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
   | lrsp_leaf : forall v t e ,

-    (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) ->
+    (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 [(v, t)] (ELR_leaf _ _ _ _ _ t e)
   | lrsp_cons : forall t1 t2 b1 b2,
     LetRecSubproofs Γ Δ ξ lev t1 b1 ->

@@ -447,31 +953,43 @@ Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ l
 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
   LetRecSubproofs Γ Δ ξ lev tree branches ->
     ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
   LetRecSubproofs Γ Δ ξ lev tree branches ->
     ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)

-      |- eLetRecTypes branches @@@ lev ].
+      |- (mapOptionTree (@snd _ _) tree) @ lev ].

   intro X; induction X; intros; simpl in *.
     apply nd_rule.
   intro X; induction X; intros; simpl in *.
     apply nd_rule.

-      apply REmptyGroup.
+      apply RVoid.

     set (ξ v) as q in *.
       destruct q.
       simpl in *.
       apply n.
     set (ξ v) as q in *.
       destruct q.
       simpl in *.
       apply n.

-    eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
-    eapply nd_comp; [ apply nd_llecnac | idtac ].
-    apply nd_prod; auto.
-  Defined.
+    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  :
 
 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :

-    forall branches body,
-    ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] -> 
-    LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) 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 *)
   intro branches.
   intro body.
 
   (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
   intro branches.
   intro body.

+  intro disti.

   intro pf.
   intro lrsp.
   intro pf.
   intro lrsp.

-  set ((update_ξ ξ 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 ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
   set (mapOptionTree (@fst _ _) tree) as pctx.
   set (mapOptionTree ξ' pctx) as passback.

@@ -479,97 +997,87 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
   clear z.
 
   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
   clear z.
 

-  set (@arrangeContextAndWeaken''  Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
+  set (@factorContextLeftAndWeaken''  Γ Δ  pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.

   unfold passback in *; clear passback.
   unfold pctx in *; clear pctx.
   unfold passback in *; clear passback.
   unfold pctx in *; clear pctx.

-  eapply UND_to_ND in q'.
+  set (q' disti) as q''.

 
   unfold ξ' in *.
 
   unfold ξ' in *.

-  set (@updating_stripped_tree_is_inert') as zz.
-  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 ξ'.
   Opaque stripOutVars.
   simpl.
   clear zz.
   clear ξ'.
   Opaque stripOutVars.
   simpl.

-  rewrite <- mapOptionTree_compose in q'.
-  cut ((mapOptionTree (update_ξ ξ lev (leaves tree) ○ (@fst _ _)) tree) = (mapOptionTree (@snd _ _) tree @@@ lev)).
-  intro H'.
-  rewrite <- H'.
-  eapply nd_comp; [ idtac | apply q' ].
-  clear H'.
+  rewrite <- mapOptionTree_compose in q''.
+  rewrite <- ξlemma.
+  eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ _ q'') ].

   clear q'.
   clear q'.

+  clear q''.

   simpl.
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as 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.
-    cut ((eLetRecTypes branches @@@ lev) = mapOptionTree (update_ξ ξ lev (leaves tree) ○ (@fst _ _)) tree).
-      intro H''.
-      rewrite <- H''.
-    apply q.
-  admit.
-  admit.
-  admit.
-  Defined.

 
 

-Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)),
-  distinct (map (@fst _ _) varstypes) ->
-  map (update_ξ ξ lev varstypes) (map (@fst _ _) varstypes) =
-  map (fun t => t@@ lev) (map (@snd _ _) varstypes).
-  intros.
-  induction varstypes.
-  reflexivity.
-  destruct a.
-  inversion H.
-  subst.
-  admit.
-  Qed.
-
-Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
-  admit.
-  Qed.
-
-Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
-  admit.
-  Defined.
-
-Lemma vec2list_injective : forall T n (v1 v2:vec T n), vec2list v1 = vec2list v2 -> v1 = v2.
-  admit.
-  Defined.
-
-Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _} :
-  forall scb:StrongCaseBranchWithVVs _ _ tc atypes,
-    forall l ξ, vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb) =
-                                 vec_map (fun t => t @@ weakL' l) (sac_types (scbwv_sac scb) _ atypes).
+    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.
   intros.

-  unfold scbwv_ξ.
+  unfold scbwv_xi.

   unfold scbwv_varstypes.
   unfold scbwv_varstypes.

-  set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
-    (vec2list (vec_zip (scbwv_exprvars scb) (sac_types (scbwv_sac scb) Γ atypes)))) 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 vec2list_map_list2vec in q.
-  apply vec2list_injective.
-  apply q.
+  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.
 
   apply scbwv_exprvars_distinct.
   Qed.
 

-Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts',
-  mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
-  = ((mapOptionTreeAndFlatten pcb_freevars (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ  (expr2antecedent e)).
+
+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'.
   intros.
   simpl.
   Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
   hack.
   induction alts'.

-  simpl.
-  destruct a.
+  destruct a; simpl.
+  destruct s; simpl.

   unfold mkProofCaseBranch.
   unfold mkProofCaseBranch.

-  simpl.

   reflexivity.
   reflexivity.
   simpl.
   reflexivity.
   reflexivity.
   simpl.

@@ -580,69 +1088,68 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts',
   reflexivity.
   Qed.
 
   reflexivity.
   Qed.
 

-

 Definition expr2proof  :
 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
-    | EGlobal  Γ Δ ξ t wev                          => let case_EGlobal := tt in _
+  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 
     | 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 
     | 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_ξ ξ lev (leaves tree) in
-      let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) 
+                                                       (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 _ _ _ _
         ((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 t e => lrsp_leaf Γ Δ ξ l v t 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)
           | 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:
     | 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
+               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)  =>
           | 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 ○ mkProofCaseBranch) X] with
-            existT scbx ex =>
-            (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
+            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')
         end
         end) alts')

-        in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+        in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)

     end
     end

-  ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
+  ); clear exp ξ' τ' Γ' Δ' l' expr2proof; try clear mkdcsp.

 
     destruct case_EGlobal.
       apply nd_rule.
       simpl.
 
     destruct case_EGlobal.
       apply nd_rule.
       simpl.

-      destruct t as [t lev].
-      apply (RGlobal _ _ _ _ wev).
+      apply (RGlobal _ _ _  g).

 
     destruct case_EVar.
       apply nd_rule.
 
     destruct case_EVar.
       apply nd_rule.

@@ -656,25 +1163,24 @@ Definition expr2proof  :
 
     destruct case_EApp.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 
     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.
       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 ].
 
     destruct case_ELam; intros.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].

-      set (update_ξ ξ lev ((v,t1)::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.
         unfold ξ' in pfx.

-        fold (mapOptionTree (update_ξ ξ lev ((v,t1)::nil))) in pfx.

         rewrite updating_stripped_tree_is_inert in pfx.
         rewrite updating_stripped_tree_is_inert in pfx.

-        unfold update_ξ in pfx.
+        unfold update_xi in pfx.

         destruct (eqd_dec v v).
         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.
         clear pfx.
         apply e'.
         assert False.

@@ -683,25 +1189,24 @@ Definition expr2proof  :
         inversion H.
 
     destruct case_ELet; intros; simpl in *.
         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 ].
       eapply nd_comp; [ apply pf_body | idtac ].

-      clear pf_body.

       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).
       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).

-      set (update_ξ ξ v ((lev,tv)::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 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 ξ'.
       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.
       assert False. apply n0; auto. inversion H.
 
     destruct case_EEsc.

@@ -718,7 +1223,6 @@ Definition expr2proof  :
       auto.
 
     destruct case_ENote.
       auto.
 
     destruct case_ENote.

-      destruct t.

       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
       apply e'.
       auto.
       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
       apply e'.
       auto.

@@ -748,30 +1252,36 @@ Definition expr2proof  :
       clear o x alts alts' e.
       eapply nd_comp; [ apply e' | idtac ].
       clear e'.
       clear o x alts alts' e.
       eapply nd_comp; [ apply e' | idtac ].
       clear e'.

-      set (existT
-              (fun scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes =>
-               Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ))
-                 (scbwv_ξ scb ξ l) (weakLT' (tbranches @@  l))) scbx ex) as stuff.
-      set (fun q r x1 x2 y1 y2 => @UND_to_ND q r [q >> r > x1 |- y1] [q >> r > x2 |- y2]).
-      simpl in n.
-      apply n.
-      clear n.
-
+      apply nd_rule.
+      apply RArrange.
+      simpl.

       rewrite mapleaves'.
       simpl.
       rewrite <- mapOptionTree_compose.
       rewrite mapleaves'.
       simpl.
       rewrite <- mapOptionTree_compose.

-      rewrite <- updating_stripped_tree_is_inert''' with (l:=l).
-      replace (vec2list (scbwv_exprvars scbx)) with (leaves (unleaves (vec2list (scbwv_exprvars scbx)))).
+      unfold scbwv_xi.

       rewrite <- mapleaves'.
       rewrite vec2list_map_list2vec.
       rewrite <- mapleaves'.
       rewrite vec2list_map_list2vec.

-      unfold sac_Γ.      
+      unfold sac_gamma.      

       rewrite <- (scbwv_coherent scbx l ξ).
       rewrite <- vec2list_map_list2vec.
       rewrite mapleaves'.
       rewrite <- (scbwv_coherent scbx l ξ).
       rewrite <- vec2list_map_list2vec.
       rewrite mapleaves'.

-      apply arrangeContextAndWeaken''.
+      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.
       apply (scbwv_exprvars_distinct scbx).

-      apply leaves_unleaves.
+      rewrite leaves_unleaves.
+      reflexivity.

 
     destruct case_nil.
       apply nd_id0.
 
     destruct case_nil.
       apply nd_id0.

@@ -783,7 +1293,8 @@ Definition expr2proof  :
       apply b2'.
 
     destruct case_ECase.
       apply b2'.
 
     destruct case_ECase.

-      rewrite case_lemma.
+    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.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
       rewrite <- mapOptionTree_compose.