add support for flattening non-recursive Let bindings

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

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 79e16cd..8cd5688 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -16,51 +16,24 @@ Require Import HaskProof.
 
 Section HaskStrongToProof.
 
 
 Section HaskStrongToProof.
 

-(* 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.
+Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
+  RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
+
+Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
+  eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
+  eapply RComp; [ idtac | apply RCossa ]. 
+  eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
+  apply RAssoc.

   Defined.
   Defined.

-
-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.
-    simpl in *.
-    eapply nd_comp ; [ idtac | apply q ]. 
-    clear q.
-    apply nd_rule.
-    apply RAssoc.
-    Defined.
-
-

   
 Context {VV:Type}{eqd_vv:EqDecidable VV}.
 
   
 Context {VV:Type}{eqd_vv:EqDecidable VV}.
 

-  (* 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.
+(* 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.

 
 Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
   match t with 
 
 Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
   match t with 

@@ -148,31 +121,83 @@ Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOu
   reflexivity.
   Qed.
 
   reflexivity.
   Qed.
 

-Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t.
-(*
-  induction x.
-  simpl.
+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.
   unfold stripOutVars.

-  simpl.
-  rewrite mapOptionTree'_compose.

   induction t.
   induction t.

-  destruct a; try reflexivity.
-  simpl.
-  destruct (dropVar y v); reflexivity.
-  simpl.
-  rewrite IHt1.
-  rewrite IHt2.
-  reflexivity.
-  rewrite strip_lemma.
-  rewrite IHx.
-  rewrite <- strip_lemma.
-  rewrite app_comm_cons.
-  reflexivity.
-*)
-admit.
+  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 *.
+    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.
+
+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.
 
   Qed.
 

-Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
+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.
   intros.
   induction y.
   destruct a0; try reflexivity.

@@ -259,7 +284,7 @@ Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app
   auto.
   Qed.
 
   auto.
   Qed.
 

-Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
+Lemma notin_strip_inert' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.

   induction x; intros.
   simpl in H.
   unfold stripOutVars.
   induction x; intros.
   simpl in H.
   unfold stripOutVars.

@@ -277,7 +302,7 @@ Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars
   set (IHx H3) as qq.
   rewrite strip_lemma.
   rewrite IHx.
   set (IHx H3) as qq.
   rewrite strip_lemma.
   rewrite IHx.

-  apply strip_distinct.
+  apply notin_strip_inert.

   unfold not; intros.
   apply H2.
   apply In_both'.
   unfold not; intros.
   apply H2.
   apply In_both'.

@@ -285,50 +310,216 @@ Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars
   auto.
   Qed.
 
   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_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
   = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
 Lemma updating_stripped_tree_is_inert'
   {Γ} lev
   (ξ:VV -> LeveledHaskType Γ ★)
   lv tree2 :
     mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
   = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).

+

   induction tree2.
   induction tree2.

-  destruct a.
-  simpl.
-  induction lv.
-  reflexivity.
-  simpl.
-  destruct a.
-  simpl.
-  set (eqd_dec v v0) as q.
-  destruct q.
-  auto.
-  set (dropVar (map (@fst _ _) lv) v) as b in *.
-  destruct b.
-  inversion IHlv.
-  admit.
-  auto.
-  reflexivity.
+    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.
   simpl.

-  unfold stripOutVars in *.
-  rewrite <- IHtree2_1.
-  rewrite <- IHtree2_2.
-  reflexivity.
+  right; auto.

   Qed.
 
   Qed.
 

-Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)),
-  distinct (map (@fst _ _) (leaves varstypes)) ->
-  mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
-  mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
-  admit.
+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.
 
   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_ξ_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
+  forall v1 v2,
+  distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) ->
+  mapOptionTree (update_ξ ξ 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_ξ_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
+  distinct (map (@fst _ _) (leaves varstypes)) ->
+  mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
+  mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
+  set (update_ξ_lemma' Γ ξ lev varstypes [] []) as q.
+  simpl in q.
+  rewrite <- app_nil_end in q.
+  apply q.
+  Qed.

 
 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
   match exp as E in Expr Γ Δ ξ τ with
 
 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
   match exp as E in Expr Γ Δ ξ τ with

-  | EGlobal  Γ Δ ξ _ _                            => []
+  | EGlobal  Γ Δ ξ _ _ _                          => []

   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)

@@ -342,7 +533,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ?
   | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => expr2antecedent e
   | ECoApp   Γ Δ κ γ σ₁ σ₂ σ ξ l      e           => expr2antecedent e
   | ETyApp   Γ Δ κ σ τ ξ  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     stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
       let branch_context := eLetRecContext branches
    in let all_contexts := (expr2antecedent body),,branch_context
    in     stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts

@@ -390,21 +581,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}

@@ -422,23 +598,22 @@ Lemma stripping_nothing_is_inert
     reflexivity.
     Qed.
 
     reflexivity.
     Qed.
 

-Definition arrangeContext 
+Definition arrangeContext

      (Γ: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.
   

@@ -455,18 +630,15 @@ Definition arrangeContext
             (* where the leaf is v *)
             apply inr.
               subst.
             (* where the leaf is v *)
             apply inr.
               subst.

-              apply nd_rule.

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

-              apply nd_rule.

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

-          apply nd_rule.

           apply RuCanR.
   
       (* branch *)
           apply RuCanR.
   
       (* branch *)

@@ -486,87 +658,73 @@ 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 RComp; [idtac | apply RuCanR ].
+        exact (RComp

           (* 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 _ _ _ _))))).
+          (RRight _ (RComp lpf (RCanR _)))
+          (RLeft  _ (RComp rpf (RCanR _)))).

 
 
     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 (RRight (mapOptionTree ξ ctx2)  (RComp lpf ((RCanR _)))) as q.

       simpl in *.
       simpl in *.

-      eapply nd_comp.
+      eapply RComp.

       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 RComp; [ idtac | apply RAssoc ].
+      apply RLeft.

       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 RComp; [ idtac | eapply pivotContext ].
+      set (RComp rpf (RCanR _ )) as rpf'.
+      set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.

       simpl in *.
       simpl in *.

-      eapply nd_comp; [ idtac | apply qq ].
+      eapply RComp; [ 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 (RRight (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 RComp; [ idtac | eapply copyAndPivotContext ].
+        (* order will not matter because these are central as morphisms *)
+        exact (RComp (RRight _ lpf) (RLeft _ rpf)).

 
     Defined.
 
 (* same as before, but use RWeak if necessary *)
 
     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.
+Definition arrangeContextAndWeaken  
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     ctx    (* initial context *)
+     (ξ:VV -> LeveledHaskType Γ ★) :
+       Arrange
+          (mapOptionTree ξ                        ctx                )
+          (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        ).
+  set (arrangeContext Γ Δ 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 RComp; [ apply a | idtac ].
+  refine (RLeft _ (RWeak _)).

   Defined.
 
   Defined.
 

-Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
-      mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
-    = mapOptionTree ξ (stripOutVars (v :: nil) tree).
-  set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
-  rewrite p.
-  simpl.
-  reflexivity.
-  Qed.
-
-Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
-  admit.
-  Qed.
-
-Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, 
+Definition arrangeContextAndWeaken''
+     (Γ: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.

@@ -575,11 +733,11 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
     fold (mapOptionTree ξ) in *.
     intros.
     apply arrangeContextAndWeaken.
     fold (mapOptionTree ξ) in *.
     intros.
     apply arrangeContextAndWeaken.

+    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.
     intros.
     unfold mapOptionTree in *.
     apply RuCanR.
     intros.
     unfold mapOptionTree in *.

@@ -587,7 +745,7 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
     fold (mapOptionTree ξ) in *.
     set (mapOptionTree ξ) as X 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'.

@@ -599,20 +757,28 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
     fold X in IHv2'.
     set (distinct_app _ _ _ H) as H'.
     destruct H' as [H1 H2].
     fold X in IHv2'.
     set (distinct_app _ _ _ H) as H'.
     destruct H' as [H1 H2].

-    set (nd_comp (IHv1 _ _ H1) (IHv2' H2)) as qq.
-    eapply nd_comp.
+    set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
+    eapply RComp.

       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' v1 (leaves v2)).
-        apply nd_rule.
+      rewrite (notin_strip_inert' v1 (leaves v2)).

         apply RCossa.
         apply RCossa.

-        apply cheat.
+        apply distinct_swap.

         auto.
     Defined.
 
         auto.
     Defined.
 

-(* IDEA: use multi-conclusion proofs instead *)
+Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
+      mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
+    = mapOptionTree ξ (stripOutVars (v :: nil) tree).
+  set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
+  rewrite p.
+  simpl.
+  reflexivity.
+  Qed.
+
+(* 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 ,

@@ -629,22 +795,21 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
       |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
   intro X; induction X; intros; simpl in *.
     apply nd_rule.
       |- (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 *.
       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; [ idtac | eapply nd_rule; apply RJoin ].

     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.
   Defined.
 
 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.
   Defined.
 
 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :

-    forall branches body,
-    distinct (leaves (mapOptionTree (@fst _ _) tree)) ->
+    forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),

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

@@ -653,8 +818,11 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
   intro pf.
   intro lrsp.
 
   intro pf.
   intro lrsp.
 

-  rewrite mapleaves in disti.
-  set (@update_ξ_lemma _ Γ ξ lev tree disti) as ξlemma.
+  assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'.
+    apply disti.
+    rewrite mapleaves in disti'.
+
+  set (@update_ξ_lemma _ Γ ξ lev tree disti') as ξlemma.

     rewrite <- mapOptionTree_compose in ξlemma.
 
   set ((update_ξ ξ lev (leaves tree))) as ξ' in *.
     rewrite <- mapOptionTree_compose in ξlemma.
 
   set ((update_ξ ξ lev (leaves tree))) as ξ' in *.

@@ -665,35 +833,32 @@ 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 (@arrangeContextAndWeaken''  Γ Δ  pctx ξ' (expr2antecedent body,,eLetRecContext branches)) 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 *.
   set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
   rewrite <- mapleaves in zz.
 
   unfold ξ' in *.
   set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
   rewrite <- mapleaves in zz.

-  rewrite zz in q'.
+  rewrite zz in q''.

   clear zz.
   clear ξ'.
   Opaque stripOutVars.
   simpl.
   clear zz.
   clear ξ'.
   Opaque stripOutVars.
   simpl.

-  rewrite <- mapOptionTree_compose in q'.
+  rewrite <- mapOptionTree_compose in q''.

   rewrite <- ξlemma.
   rewrite <- ξlemma.

-  eapply nd_comp; [ idtac | apply q' ].
+  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; [ idtac | eapply nd_rule; apply RJoin ].

     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.
     rewrite ξlemma.
     apply q.
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.
     rewrite ξlemma.
     apply q.

-    clear q'.
-
-  rewrite <- mapleaves in disti.
-    apply disti.

     Defined.
 
 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
     Defined.
 
 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :

@@ -764,7 +929,7 @@ Definition expr2proof  :
   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
     match exp as E in Expr Γ Δ ξ τ with
   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 _
+    | 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 

@@ -772,7 +937,7 @@ Definition expr2proof  :
     | 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) 
     | 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      =>
+    | ELetRec  Γ Δ ξ lev t tree disti branches ebody =>

       let ξ' := update_ξ ξ lev (leaves tree) in
       let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) 
         ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
       let ξ' := update_ξ ξ lev (leaves tree) in
       let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) 
         ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))

@@ -818,8 +983,7 @@ Definition expr2proof  :
     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.

@@ -843,15 +1007,14 @@ Definition expr2proof  :
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
       set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
       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 (arrangeContextAndWeaken Γ Δ 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.
         unfold update_ξ in pfx.
         destruct (eqd_dec v v).
         rewrite updating_stripped_tree_is_inert in pfx.
         unfold update_ξ 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.
         clear pfx.
         apply e'.
         assert False.

@@ -862,14 +1025,15 @@ Definition expr2proof  :
     destruct case_ELet; intros; simpl in *.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
     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; [ apply pf_body | idtac ].
-      clear pf_body.
+      apply nd_prod.
+        apply pf_let.
+        clear pf_let.
+        eapply nd_comp; [ apply pf_body | idtac ].
+        clear pf_body.

       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).
       set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).
       set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.

-      set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
+      set (arrangeContextAndWeaken Γ Δ 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.

@@ -877,8 +1041,8 @@ Definition expr2proof  :
       destruct (eqd_dec lev lev).
       unfold ξ'.
       unfold update_ξ.
       destruct (eqd_dec lev lev).
       unfold ξ'.
       unfold update_ξ.

-      apply UND_to_ND in n.
-      apply n.
+      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.

@@ -925,11 +1089,9 @@ 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 (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.

@@ -951,6 +1113,7 @@ Definition expr2proof  :
       replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
         (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
       apply q.
       replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
         (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
       apply q.

+      apply (sac_Δ sac Γ atypes (weakCK'' Δ)).

       rewrite leaves_unleaves.
       apply (scbwv_exprvars_distinct scbx).
       rewrite leaves_unleaves.
       rewrite leaves_unleaves.
       apply (scbwv_exprvars_distinct scbx).
       rewrite leaves_unleaves.

@@ -980,7 +1143,6 @@ Definition expr2proof  :
       unfold ξ'1 in *.
       clear ξ'1.
       apply letRecSubproofsToND'.
       unfold ξ'1 in *.
       clear ξ'1.
       apply letRecSubproofsToND'.

-      admit.

       apply e'.
       apply subproofs.
 
       apply e'.
       apply subproofs.