diff --git a/theories/LogicalRelation/Application.v b/theories/LogicalRelation/Application.v
index 1f3fa20..2a2c7ac 100644
--- a/theories/LogicalRelation/Application.v
+++ b/theories/LogicalRelation/Application.v
@@ -1,7 +1,7 @@
-Require Import PeanoNat.
+
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations LContexts Context NormalForms Weakening GenericTyping LogicalRelation DeclarativeInstance.
-From LogRel.LogicalRelation Require Import Induction Irrelevance Escape Reflexivity Weakening Neutral Transitivity Reduction NormalRed.
+From LogRel Require Import Utils BasicAst Notations LContexts Context NormalForms Weakening GenericTyping Monad LogicalRelation.
+From LogRel.LogicalRelation Require Import Split Induction Irrelevance Escape Reflexivity Weakening Monotonicity Neutral Transitivity Reduction NormalRed.
 
 Set Universe Polymorphism.
 
@@ -14,552 +14,61 @@ Context `{GenericTypingProperties}.
 
 Set Printing Primitive Projection Parameters.
 
-Record helpTy2 {Γ F G l} (wl : wfLCon) (WN : nat)
-  :=
-  { f : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-      wfLCon;
-    ub : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-      f wl' tau ne ≤ε wl ;
-    lesser : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-      wl' ≤ε f wl' tau ne ;
-    ne : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-      AllInLCon WN (f wl' tau ne) ;
-    dom2 : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-      term ;
-    cod2 : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-      term ;
-    red2 : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-      [Γ |-[ ta ] tProd F G :⇒*: tProd (dom2 wl' tau ne) (cod2 wl' tau ne) ]< (f wl' tau ne) > ;
-    domTy2 : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-      [Γ |-[ ta ] (dom2 wl' tau ne) ]< (f wl' tau ne) > ;
-    codTy2 : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-      [Γ ,, (dom2 wl' tau ne) |-[ ta ] (cod2 wl' tau ne) ]< (f wl' tau ne) > ;
-    eq2 : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-      [Γ |-[ ta ] tProd (dom2 wl' tau ne) (cod2 wl' tau ne) ≅
-             tProd (dom2 wl' tau ne) (cod2 wl' tau ne)]< (f wl' tau ne) > ;
-    domN2 : nat ;
-    domRed2 : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-    forall (Δ : context) (l' : wfLCon) (ρ : Δ ≤ Γ),
-           l' ≤ε (f wl' tau ne) ->
-           AllInLCon (domN2) l' -> [ |-[ ta ] Δ ]< l' > ->
-           [Δ ||-< l > (dom2 wl' tau ne)⟨ρ⟩ ]< l' > ;
-    codomN2 : forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-    forall (Δ : context) (a : term) (l' : wfLCon) (ρ : Δ ≤ Γ)
-             (τ : l' ≤ε (f wl' tau ne))
-             (Ninfl : AllInLCon (domN2) l') (h : [ |-[ ta ] Δ ]< l' >),
-      [domRed2 wl' tau ne Δ l' ρ τ Ninfl h | Δ ||- a : (dom2 wl' tau ne)⟨ρ⟩ ]< l' > -> nat ;
-(*    codomN2_Ltrans :
-    forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-    forall (Δ : context) (a : term) (l' l'' : wfLCon) 
-           (ρ : Δ ≤ Γ)
-           (τ : l' ≤ε (f wl' tau ne))
-           (τ' : l'' ≤ε (f wl' tau ne))
-           (Ninfl : AllInLCon (domN2) l')
-           (Ninfl' : AllInLCon (domN2) l'')
-           (h : [ |-[ ta ] Δ ]< l' >) (h' : [ |-[ ta ] Δ ]< l'' >)
-           (ha : [domRed2 wl' tau ne Δ l' ρ τ Ninfl h | Δ ||- a : (dom2 wl' tau ne)⟨ρ⟩ ]< l' >)
-           (ha' : [domRed2 wl' tau ne Δ l'' ρ τ' Ninfl' h' | Δ ||- a : (dom2 wl' tau ne)⟨ρ⟩ ]< l'' >),
-      l'' ≤ε l' ->
-      codomN2 wl' tau ne Δ a l'' ρ τ' Ninfl' h' ha' <=
-        codomN2 wl' tau ne Δ a l' ρ τ Ninfl h ha ;
-    codomN2_Ltrans' :
-    forall (wl' wl'' : wfLCon) (tau : wl' ≤ε wl) (tau' : wl'' ≤ε wl)
-           (ne : AllInLCon WN wl') (ne' : AllInLCon WN wl''),
-    forall (Δ : context) (a : term) (l': wfLCon) 
-           (ρ : Δ ≤ Γ)
-           (τ : l' ≤ε (f wl' tau ne))
-           (τ' : l' ≤ε (f wl'' tau' ne'))
-           (Ninfl : AllInLCon domN2 l')
-           (h : [ |-[ ta ] Δ ]< l' >)
-           (ha : [domRed2 wl' tau ne Δ l' ρ τ Ninfl h | Δ ||- a : (dom2 wl' tau ne)⟨ρ⟩ ]< l' >)
-           (ha' : [domRed2 wl'' tau' ne' Δ l' ρ τ' Ninfl h | Δ ||- a : (dom2 wl'' tau' ne')⟨ρ⟩ ]< l' >),
-      wl'' ≤ε wl' ->
-      codomN2 wl'' tau' ne' Δ a l' ρ τ' Ninfl h ha' <=
-        codomN2 wl' tau ne Δ a l' ρ τ Ninfl h ha ;*)
-    codRed2 :
-    forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-    forall (Δ : context) (a : term) (l' : wfLCon) (ρ : Δ ≤ Γ)
-             (τ : l' ≤ε (f wl' tau ne))
-             (Ninfl : AllInLCon (domN2) l')
-             (h : [ |-[ ta ] Δ ]< l' >)
-             (ha : [domRed2 wl' tau ne Δ l' ρ τ Ninfl h | Δ ||- a : (dom2 wl' tau ne)⟨ρ⟩ ]< l' >) 
-             (l'' : wfLCon),
-      l'' ≤ε l' ->
-      AllInLCon (codomN2 wl' tau ne Δ a l' ρ τ Ninfl h ha) l'' ->
-      [Δ ||-< l > (cod2 wl' tau ne)[a .: ρ >> tRel] ]< l'' > ;
-    codExt2 :
-    forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-    forall (Δ : context) (a b : term) (l' : wfLCon) (ρ : Δ ≤ Γ)
-             (τ : l' ≤ε (f wl' tau ne))
-             (Ninfl : AllInLCon domN2 l')
-             (h : [ |-[ ta ] Δ ]< l' >)
-             (ha : [domRed2 wl' tau ne Δ l' ρ τ Ninfl h | Δ ||- a : (dom2 wl' tau ne)⟨ρ⟩ ]< l' >),
-           [domRed2 wl' tau ne Δ l' ρ τ Ninfl h | Δ ||- b : (dom2 wl' tau ne)⟨ρ⟩ ]< l' > ->
-           [domRed2 wl' tau ne Δ l' ρ τ Ninfl h | Δ ||- a ≅ b : (dom2 wl' tau ne)⟨ρ⟩ ]< l' > ->
-           forall (l'' : wfLCon) (τ' : l'' ≤ε l')
-             (Minfl : AllInLCon (codomN2 wl' tau ne Δ a l' ρ τ Ninfl h ha) l''),
-             [codRed2 wl' tau ne Δ a l' ρ τ Ninfl h ha l'' τ' Minfl |
-               Δ ||- (cod2 wl' tau ne)[a .: ρ >> tRel] ≅
-                 (cod2 wl' tau ne)[b .: ρ >> tRel] ]< l'' > ;
-  }.
-
 
 Section AppTerm.
-  Context {wl Γ t u F G l l'}
+  Context {wl Γ t u F G l l' l''}
     (hΠ : [Γ ||-Π<l> tProd F G]< wl >)
-    {RFN : nat}
-    {RF : forall wl' (τ : wl' ≤ε wl) (Ninfl : AllInLCon RFN wl'),
-        [Γ ||-<l'> F]< wl' > }
-    (Rt : [Γ ||-<l> t : tProd F G | LRPi' (hΠ)]< wl >)
-    (RuN : nat)
-    (Ru : forall wl' (τ : wl' ≤ε wl)
-                 (Ninfl : AllInLCon RFN wl')
-                 (Ninfl' : AllInLCon RuN wl'),
-        [Γ ||-<l'> u : F | RF wl' τ Ninfl ]< wl' >)
-  (*  (RGu : W[Γ ||-<l''> G[u..]]< wl >) *).
-    
-  Definition AppTyN : nat.
-  Proof.
-    refine (max (max (max RFN RuN)
-               (max (PiRedTyPack.domN hΠ) (PiRedTm.redN Rt))) _).
-    unshelve refine (Max_Bar _ _ _).
-    About Max_Bar_Bar_lub.
-    + assumption.
-    + exact (max (max RFN RuN)
-               (max (PiRedTyPack.domN hΠ) (PiRedTm.redN Rt))).
-    + intros.
-      unshelve eapply (PiRedTyPack.codomN hΠ).
-      * assumption.
-      * exact u.
-      * exact wl'.
-      * exact wk_id.
-      * assumption.
-      * (eapply AllInLCon_le ; [ | eassumption] ;
-                  eapply Nat.max_lub_l ;
-                  now eapply Nat.max_lub_r).
-      * eapply wfc_Ltrans ; try eassumption.
-        exact (wfc_wft (PiRedTyPack.domTy hΠ)).
-      * abstract (irrelevance0 ;
-                  [ | unshelve eapply Ru ; try eassumption ;
-                      eapply AllInLCon_le ;
-                      [ eapply Nat.max_lub_l ;
-                        now eapply Nat.max_lub_l | eassumption |
-                        eapply Nat.max_lub_r ;
-                        now eapply Nat.max_lub_l | eassumption]] ;
-         assert (tProd (PiRedTyPack.dom hΠ) (PiRedTyPack.cod hΠ) =
-                   tProd F G) as ePi ;
-         [pose proof (eq := (PiRedTyPack.red hΠ)) ;
-          eapply whredty_det ; now gen_typing |
-           inversion ePi ; now bsimpl]).
-  Defined.
-About AppTyN_subproof.
-    
+    {RF : [Γ ||-<l'> F]< wl >}
+    (Rt : [Γ ||-<l> t : tProd F G | LRPi' (normRedΠ0 hΠ)]< wl >)
+    (Ru : [Γ ||-<l'> u : F | RF]< wl >)
+    (RGu : W[Γ ||-<l''> G[u..]]< wl >).
 
-  Definition AppTy : W[Γ ||-<l> G[u..]]< wl >.
+  Lemma app_id : W[Γ ||-<l''> tApp (PiRedTm.nf Rt) u : G[u..] | RGu]< wl >.
   Proof.
-    exists AppTyN.
-    pose proof (r:= PiRedTyPack.red hΠ). 
-    assert (tProd (PiRedTyPack.dom hΠ) (PiRedTyPack.cod hΠ) = tProd F G) as ePi
-        by (eapply whredty_det ; gen_typing) ; clear r.
-    inversion ePi ; subst ; clear ePi.
-    pose proof (wfΓ := wfc_wft (PiRedTyPack.domTy hΠ)).
-    intros.
-    replace ((PiRedTyPack.cod hΠ)[u..]) with ((PiRedTyPack.cod hΠ)[u .: _wk_id Γ >> tRel]) by now bsimpl.
-    unshelve eapply ((PiRedTyPack.codRed hΠ) wk_id).
-    - unshelve eapply (Bar_lub wl wl' _ τ).
-      exact (max (max RFN RuN)
-               (max (PiRedTyPack.domN hΠ) (PiRedTm.redN Rt))).
-      (eapply AllInLCon_le ; try eassumption ;
-                unfold AppTyN ;
-                now eapply Nat.le_max_l).
-    - now eapply Bar_lub_ub.
-    - (eapply AllInLCon_le ; [ | now eapply Bar_lub_AllInLCon] ;
-                  eapply Nat.max_lub_l ;
-                  now eapply Nat.max_lub_r).
-    - (eapply (wfc_Ltrans)).
-      2: exact (wfc_wft (PiRedTyPack.domTy hΠ)).
-      now eapply Bar_lub_ub.
-    - now eapply (AppTyN_subproof).
-    - now eapply Bar_lub_smaller.
-    - cbn.
-      eapply AllInLCon_le.
-      2: eassumption.
-      unfold AppTyN.
-      etransitivity.
-      2: now eapply Nat.max_lub_r.
-      etransitivity.
-      2: { unshelve eapply (Max_Bar_Bar_lub).
-           2: eassumption.
-           + (eapply AllInLCon_le ; try eassumption ;
-                unfold AppTyN ;
-                now eapply Nat.le_max_l).
-           + now eapply Bar_lub_ub. 
-           + now eapply Bar_lub_AllInLCon.
-      }
-      reflexivity.
-      Defined. 
-      
-  Definition app_idN : nat.
-  Proof.
-    refine (max (max (max RFN RuN) (max (PiRedTyPack.domN hΠ) (PiRedTm.redN Rt))) _).
-    unshelve eapply Max_Bar.
-    - exact wl.
-    - exact (max (max RFN RuN) (max (PiRedTyPack.domN hΠ) (PiRedTm.redN Rt))).
-    - intros.
-      unshelve eapply (PiRedTm.appN Rt).
-      + assumption.
-      + exact u.
-      + exact wl'.
-      + now eapply wk_id.
-      + assumption.
-      + (eapply AllInLCon_le ; [ | eassumption] ;
-                  eapply Nat.max_lub_l ;
-         now eapply Nat.max_lub_r).
-      + eapply wfc_Ltrans ; try eassumption.
-        exact (wfc_wft (PiRedTyPack.domTy hΠ)).
-      + eapply AllInLCon_le ; [ | eassumption].
-        eapply Nat.max_lub_r ; now eapply Nat.max_lub_r.
-      + eapply AppTyN_subproof.
-Defined.
-  
-  Lemma app_id_aux :
-    W[Γ ||-<l> tApp (PiRedTm.nf Rt) u : G[u..] | AppTy]< wl >.
-  Proof.
-    exists app_idN.
-    intros.
+    assert (wfΓ := wfc_wft (escape RF)).
     replace (PiRedTm.nf _) with (PiRedTm.nf Rt)⟨@wk_id Γ⟩ by now bsimpl.
-    irrelevance0.  2: unshelve eapply (PiRedTm.app Rt).
-    cbn.
-    abstract (assert (tProd (PiRedTyPack.dom hΠ) (PiRedTyPack.cod hΠ) = tProd F G) as ePi ;
-              [ pose proof (red := (PiRedTyPack.red hΠ)) ;
-                eapply whredty_det ; now gen_typing |
-                inversion ePi ; subst ; 
-                now bsimpl]).
-    - unshelve eapply (Bar_lub wl wl' _ τ).
-      + exact (max (max RFN RuN) (max (PiRedTyPack.domN hΠ) (PiRedTm.redN Rt))).
-      + (eapply AllInLCon_le ; try eassumption ;
-                unfold AppTyN ;
-                now eapply Nat.le_max_l).
-    - now eapply Bar_lub_ub.
-    - (eapply AllInLCon_le ; [ | now eapply Bar_lub_AllInLCon] ;
-                  eapply Nat.max_lub_l ;
-       now eapply Nat.max_lub_r).
-    - (eapply (wfc_Ltrans)).
-      2: exact (wfc_wft (PiRedTyPack.domTy hΠ)).
-      now eapply Bar_lub_ub.
-    - eapply AppTyN_subproof.
-    - now eapply Bar_lub_smaller.
-    - cbn.
-      unfold NormalRed.normRedΠ0_obligation_7.
-      cbn.
-      eapply AllInLCon_le ; [ | exact Ninfl].
-      unfold AppTy ; cbn ; unfold AppTyN ; cbn.
-      etransitivity.
-      2:{eapply Nat.max_lub_r.
-         cbn ; unfold AppTyN.
-         reflexivity. }
-      etransitivity.
-      2:{ unshelve eapply (Max_Bar_Bar_lub).
+    unshelve econstructor.
+    - eapply DTree_fusion.
+      + unshelve eapply (PiRedTm.appTree Rt wk_id (wfLCon_le_id _)).
+        2: eassumption.
+        * exact u.
+        * cbn in *.
+          irrelevance0.
           2: eassumption.
-          + (eapply AllInLCon_le ; try eassumption ;
-                unfold AppTyN ;
-                now eapply Nat.le_max_l).
-          + now eapply Bar_lub_ub.
-          + now eapply Bar_lub_AllInLCon.
-          + clear Ninfl Ninfl' τ wl'.
-             (intros ;
-              rewrite (AllInLCon_Irrel _ _ ne0 ne') ;
-              rewrite (wfLCon_le_Irrel _ _ τ τ');
-              reflexivity). }
-      reflexivity.
-    - eapply AllInLCon_le.
-      2: eapply Bar_lub_AllInLCon.
-      eapply Nat.max_lub_r ; now eapply Nat.max_lub_r. 
-    - cbn.
-      eapply AllInLCon_le ; [ | eassumption].
-      etransitivity.
-      2:{unfold app_idN.
-         eapply Nat.max_lub_r.
-         reflexivity. }
-      etransitivity.
-      2:{ unshelve eapply Max_Bar_Bar_lub.
-          + exact wl'.
-          + assumption.
-          + (eapply AllInLCon_le ; try eassumption ;
-                unfold AppTyN ;
-                now eapply Nat.le_max_l). 
-          + now eapply Bar_lub_ub.
-          + cbn. now eapply Bar_lub_AllInLCon.
-          + clear Ninfl Ninfl' τ wl'.
-            intros ;
-              rewrite (AllInLCon_Irrel _ _ ne0 ne') ;
-              rewrite (wfLCon_le_Irrel _ _ τ τ');
-              reflexivity.
-      }
-      cbn.
-      reflexivity.
-Qed.        
-
-  Lemma app_id {l''} (RGu : W[Γ ||-<l''> G[u..]]< wl >):
-    W[Γ ||-<l''> tApp (PiRedTm.nf Rt) u : G[u..] | RGu]< wl >.
-  Proof.
-    eapply WLRTmRedIrrelevantCum.
-    exact app_id_aux.
+          now bsimpl.
+      + eapply (PolyRedPack.posTree (normRedΠ0 hΠ) wk_id (wfLCon_le_id _) wfΓ).
+        irrelevance0.
+        2: eassumption.
+        cbn ; now bsimpl.
+    - intros.
+      irrelevance0.
+      2: unshelve eapply (PiRedTm.app Rt wk_id (wfLCon_le_id _) wfΓ).
+      cbn; now bsimpl.
+      2: now eapply over_tree_fusion_r.
+      now eapply over_tree_fusion_l.
   Qed.
-
-  Lemma WappTerm0 {l''} (RGu : W[Γ ||-<l''> G[u..]]< wl >):
+  
+  Lemma appTerm0 :
       W[Γ ||-<l''> tApp t u : G[u..] | RGu]< wl >
       × W[Γ ||-<l''> tApp t u ≅ tApp (PiRedTm.nf Rt) u : G[u..] | RGu]< wl >.
   Proof.
-    Print redwfSubstTerm.
-    split.
-    - destruct (app_id RGu).
-      exists (max (max RuN WNTm) RFN).
-      intros.
-      eapply redwfSubstTerm.
-      + eapply WRedTm ; try eassumption.
-        eapply AllInLCon_le ; [ | exact Ninfl'].
-        eapply Nat.max_lub_r ; now eapply Nat.max_lub_l.
-      + escape.
-        unshelve eapply redtmwf_app ; [ exact F |..].
-        destruct Rt ; cbn in *.
-        destruct hΠ ; cbn in *.
-        split.
-        * eapply ty_Ltrans ; try eassumption.
-          destruct red.
-          eapply ty_exp.
-          -- eassumption.
-          -- now destruct red0.
-        * eapply redtm_Ltrans ; try eassumption.
-          eapply redtm_conv.
-          -- now destruct red.
-          -- unshelve eapply convty_exp.
-             5 : exact eq0.
-             ++ eapply redty_refl.
-                gen_typing.
-             ++ now destruct red0. 
-        * eapply escapeTerm.
-          unshelve eapply Ru ; try eassumption.
-          eapply AllInLCon_le ; [ | exact Ninfl'].
-          now eapply Nat.max_lub_r.
-          eapply AllInLCon_le ; [ | exact Ninfl'].
-          eapply Nat.max_lub_l ; now eapply Nat.max_lub_l.
-    - destruct (app_id RGu).
-      exists (max (max RuN WNTm) RFN).
-      intros.
-      eapply redwfSubstTerm.
-      + eapply WRedTm ; try eassumption.
-        eapply AllInLCon_le ; [ | exact Ninfl'].
-        eapply Nat.max_lub_r ; now eapply Nat.max_lub_l.
-      + escape.
-        eapply redtmwf_app.
-        destruct Rt ; cbn in *.
-        destruct hΠ ; cbn in *.
-        split.
-        * eapply ty_Ltrans ; try eassumption.
-          destruct red.
-          eapply ty_exp.
-          -- eassumption.
-          -- now destruct red0.
-        * eapply redtm_Ltrans ; try eassumption.
-          eapply redtm_conv.
-          -- now destruct red.
-          -- unshelve eapply convty_exp.
-             5 : exact eq0.
-             ++ eapply redty_refl.
-                gen_typing.
-             ++ now destruct red0. 
-        * eapply escapeTerm.
-          unshelve eapply Ru ; try eassumption.
-          eapply AllInLCon_le ; [ | exact Ninfl'].
-          now eapply Nat.max_lub_r.
-          eapply AllInLCon_le ; [ | exact Ninfl'].
-          eapply Nat.max_lub_l ; now eapply Nat.max_lub_l.
+    eapply WredSubstTerm.
+    1: unshelve eapply app_id; tea.
+    escape.
+    eapply redtmwf_app.
+    1: apply Rt.
+    easy.
   Qed.
   
-
 End AppTerm.
 
-
-Definition help {wl Γ F G l} (WN : nat)
-  (WRed : forall wl' : wfLCon, wl' ≤ε wl ->
-                               AllInLCon WN wl' ->
-                               [Γ ||-Π< l > tProd F G ]< wl' >) :
-  helpTy2 (Γ := Γ) (F := F) (G := G) (l := l) wl WN.
-Proof.
-  unshelve econstructor.
-  - intros wl' τ Ninfl.
-    exact (Bar_lub wl wl' WN τ Ninfl).
-  - intros.
-    refine (PiRedTyPack.dom _).
-    unshelve eapply WRed.
-    unshelve eapply Bar_lub_ub ; try eassumption.
-    unshelve eapply Bar_lub_AllInLCon.
-  - intros.
-    refine (PiRedTyPack.cod _).
-    unshelve eapply WRed.
-    unshelve eapply Bar_lub_ub ; try eassumption.
-    unshelve eapply Bar_lub_AllInLCon.
-  - intros.
-    unshelve eapply Max_Bar.
-    + exact wl.
-    + exact WN.
-    + intros * tau Ninfl.
-      refine (PiRedTyPack.domN _).
-      unshelve eapply WRed ; try eassumption.
-  - cbn.
-    intros * τ Ninfl h.
-    refine (PiRedTyPack.domRed _ _ _ _ _) ; try eassumption.
-    eapply AllInLCon_le ; [ | exact Ninfl].
-    unshelve eapply
-      (Max_Bar_Bar_lub _ _ (fun wl'0 tau0 Ninfl0 =>
-                              PiRedTyPack.domN (WRed wl'0 tau0 Ninfl0))).
-    (intros ;
-     rewrite (AllInLCon_Irrel _ _ ne1 ne') ;
-     now rewrite (wfLCon_le_Irrel _ _ τ0 τ')).
-  - cbn.
-    intros * ha.
-    refine (PiRedTyPack.codomN _ _ _ _ _ _) ; try eassumption.
-  - cbn.
-    intros * τ' Minfl.
-    refine (PiRedTyPack.codRed _ _ _ _ _ _ _ _) ; try eassumption.
-  - cbn.
-    intros.
-    now eapply Bar_lub_ub.
-  - cbn ; intros.
-    now eapply Bar_lub_smaller.
-  - cbn ; intros.
-    now eapply Bar_lub_AllInLCon.
-  - cbn.
-    intros.
-    refine (PiRedTyPack.red _) ; try eassumption.
-  - cbn.
-    intros.
-    refine (PiRedTyPack.domTy _) ; try eassumption.
-  - cbn.
-    intros.
-    refine (PiRedTyPack.codTy _) ; try eassumption.
-  - cbn.
-    intros.
-    refine (PiRedTyPack.eq _) ; try eassumption.
-  - cbn ; intros * hb hab *.
-    eapply (PiRedTyPack.codExt _) ; try eassumption.
-Qed.
-
-Lemma test {wl Γ F G l}
-  (RΠ : W[Γ ||-<l> tProd F G]< wl >)
-  : [Γ ||-Π< l > tProd F G ]< wl >.
-Proof.
-  destruct RΠ.
-  destruct (help _ (fun wl' tau Ninfl => invLRΠ (WRed wl' tau Ninfl))).
-  assert (forall (wl' : wfLCon) (tau : wl' ≤ε wl) (ne : AllInLCon WN wl'),
-             tProd F G = tProd (dom3 wl' tau ne) (cod3 wl' tau ne)) as ePi.
-  intros.
-  1:{ now eapply whredty_det ; gen_typing . }
-  unshelve econstructor.
-  - exact F.
-  - exact G.
-  - exact (max WN domN3).
-  - intros * ? ? h.
-    eapply LRCumulative'.
-    2: {unshelve eapply domRed3 ; try eassumption.
-        + eapply AllInLCon_le ; [ | exact Ninfl].
-          now eapply Nat.le_max_l.
-        + now eapply lesser0.
-        + eapply AllInLCon_le ; [ | exact Ninfl].
-          now eapply Nat.le_max_r. }
-    + abstract
-        (specialize ePi with wl' τ (AllInLCon_le WN (Init.Nat.max WN domN3) (Nat.le_max_l WN domN3) wl' Ninfl) ;
-         now inversion ePi).
-  - cbn.
-    intros.
-    unshelve eapply codomN3 ; try eassumption.
-     + eapply AllInLCon_le ; [ | exact Ninfl].
-          now eapply Nat.le_max_l.
-     + now eapply lesser0.
-     + eapply AllInLCon_le ; [ | exact Ninfl].
-       now eapply Nat.le_max_r.
-     + irrelevance0.
-       2: exact ha.
-       exact (eq_sym (test_subproof wl Γ F G WN dom3 cod3 domN3 ePi Δ wl' ρ τ Ninfl)).
-  - cbn.
-    intros.
-    eapply LRCumulative'.
-    2:{ unshelve eapply codRed3.
-        4 : exact τ.
-        9 : exact τ'.
-        all : try eassumption. }
-    abstract
-      (pose proof (ePi' := ePi wl' τ (AllInLCon_le WN (Init.Nat.max WN domN3) (Nat.le_max_l WN domN3) wl' Ninfl)) ; now inversion ePi').
-  - econstructor.
-    2: eapply redty_refl .
-    all: unshelve eapply wft_ϝ_Bar ; try exact WN.
-    all: intros * f allinl.
-    all: unshelve eapply wft_Ltrans ; try exact (f0 wl' f allinl).
-    all: try now eapply lesser0.
-    all: destruct (red3 wl' f allinl).
-    all: now eapply redty_ty_src.
-  - unshelve eapply wft_ϝ_Bar ; try exact WN.
-    intros * f allinl.
-    unshelve eapply wft_Ltrans ; try exact (f0 wl' f allinl).
-    1: now eapply lesser0.
-    replace F with (dom3 wl' f allinl).
-    1: now eapply domTy3.
-    abstract
-        (specialize ePi with wl' f allinl ;
-         now inversion ePi).
-  - unshelve eapply wft_ϝ_Bar ; try exact WN.
-    intros * f allinl.
-    unshelve eapply wft_Ltrans ; try exact (f0 wl' f allinl).
-    1: now eapply lesser0.
-    replace F with (dom3 wl' f allinl).
-    replace G with (cod3 wl' f allinl).
-    1: now eapply codTy3.
-    all: abstract
-        (specialize ePi with wl' f allinl ;
-         now inversion ePi).
-  - unshelve eapply convty_ϝ_Bar ; try exact WN.
-    intros * f allinl.
-    unshelve eapply convty_Ltrans ; try exact (f0 wl' f allinl).
-    1: now eapply lesser0.
-    replace (tProd F G) with (tProd (dom3 wl' f allinl) (cod3 wl' f allinl)).
-    1: now eapply eq3.
-    now eapply (eq_sym (ePi _ _ _)).
-  - cbn.
-    intros * hb hab *.
-    pose proof (ePi' := ePi wl' τ (AllInLCon_le WN (Init.Nat.max WN domN3) (Nat.le_max_l WN domN3) wl' Ninfl)) ; inversion ePi' ; subst.
-    irrelevance0.
-    2:{ unshelve eapply codExt3.
-        9 : irrelevance0 ; [ | exact hb] ; reflexivity.
-        8: irrelevance0 ; [ | exact hab] ; reflexivity.
-        all: try eassumption.
-    }
-    reflexivity.
-Qed.
-      
-  
-
-Lemma appTerm {wl Γ t u F G l}
-  (RΠ : W[Γ ||-<l> tProd F G]< wl >)
-  {RF : W[Γ ||-<l> F]< wl >}
-  (Rt : W[Γ ||-<l> t : tProd F G | RΠ]< wl >)
-  (Ru : W[Γ ||-<l> u : F | RF]< wl >)
-  (RGu : W[Γ ||-<l> G[u..]]< wl >) : 
-  W[Γ ||-<l> tApp t u : G[u..]| RGu]< wl >.
-Proof.
-  unshelve eapply WappTerm0.
-  4: now eapply test.
-  8: irrelevance.
-
-
-
 Lemma appTerm {wl Γ t u F G l}
   (RΠ : [Γ ||-<l> tProd F G]< wl >)
   {RF : [Γ ||-<l> F]< wl >}
   (Rt : [Γ ||-<l> t : tProd F G | RΠ]< wl >)
   (Ru : [Γ ||-<l> u : F | RF]< wl >)
-  (RGu : [Γ ||-<l> G[u..]]< wl >) : 
-  [Γ ||-<l> tApp t u : G[u..]| RGu]< wl >.
+  (RGu : W[Γ ||-<l> G[u..]]< wl >) : 
+  W[Γ ||-<l> tApp t u : G[u..]| RGu]< wl >.
 Proof.  
   unshelve eapply appTerm0.
   7:irrelevance.
@@ -568,7 +77,71 @@ Proof.
   irrelevance.
 Qed.
 
+Lemma WappTerm {wl Γ t u F G l}
+  (hΠ : W[Γ ||-<l> tProd F G]< wl >)
+  {RF : W[Γ ||-<l> F]< wl >}
+  (Rt : W[Γ ||-<l> t : tProd F G | hΠ]< wl >)
+  (Ru : W[Γ ||-<l> u : F | RF]< wl >)
+  (RGu : W[Γ ||-<l> G[u..]]< wl >):
+  W[Γ ||-<l> tApp t u : G[u..] | RGu]< wl >.
+Proof.
+  revert RGu.
+  pattern wl.
+  unshelve eapply split_to_over_tree.
+  2:{ intros wl' n ne Ht Hf RGu.
+      unshelve eapply (TmSplit' (ne := ne)).
+      1,2: eapply WLtrans ; [ | eassumption].
+      1,2: eapply LCon_le_step ; now eapply wfLCon_le_id.
+      + unshelve eapply Ht.
+      + unshelve eapply Hf.
+  } 
+  - eapply DTree_fusion ; eapply DTree_fusion.
+    + exact (WT _ hΠ).
+    + exact (WT _ RF).
+    + exact (WTTm _ Rt).
+    + exact (WTTm _ Ru).
+  - intros wl' Hover.
+    unshelve eapply appTerm.
+    2: eapply (WRed _ hΠ).
+    + now eapply over_tree_fusion_l, over_tree_fusion_l.
+    + eapply (WRed _ RF).
+      now eapply over_tree_fusion_r, over_tree_fusion_l.
+    + eapply (WRedTm _ Rt).
+      now eapply over_tree_fusion_l, over_tree_fusion_r.
+    + eapply (WRedTm _ Ru).
+      now eapply over_tree_fusion_r, over_tree_fusion_r.
+Qed.
+
+Lemma appTerm' {wl Γ t u F G l X}
+  (hΠ : [Γ ||-<l> tProd F G]< wl >)
+  {RF : [Γ ||-<l> F]< wl >}
+  (Rt : [Γ ||-<l> t : tProd F G | hΠ]< wl >)
+  (Ru : [Γ ||-<l> u : F | RF]< wl >)
+  (eq : X = G[u..])
+  (RX : W[Γ ||-<l> X]< wl >) :
+  W[Γ ||-<l> tApp t u : X | RX]< wl >.
+Proof.
+  eapply WLRTmRedIrrelevant' ; [symmetry; tea|].
+  unshelve eapply appTerm; cycle 1; tea.
+  Unshelve. now rewrite <- eq.
+Qed.
 
+
+Lemma WappTerm' {wl Γ t u F G l X}
+  (hΠ : W[Γ ||-<l> tProd F G]< wl >)
+  {RF : W[Γ ||-<l> F]< wl >}
+  (Rt : W[Γ ||-<l> t : tProd F G | hΠ]< wl >)
+  (Ru : W[Γ ||-<l> u : F | RF]< wl >)
+  (eq : X = G[u..])
+  (RX : W[Γ ||-<l> X]< wl >) :
+  W[Γ ||-<l> tApp t u : X | RX]< wl >.
+Proof.
+  eapply WLRTmRedIrrelevant' ; [symmetry; tea|].
+  unshelve eapply WappTerm; cycle 1; tea.
+  Unshelve. now rewrite <- eq.
+Qed.
+
+  
 Lemma appcongTerm {wl Γ t t' u u' F G l l'}
   (RΠ : [Γ ||-<l> tProd F G]< wl >) 
   {RF : [Γ ||-<l'> F]< wl >}
@@ -576,47 +149,152 @@ Lemma appcongTerm {wl Γ t t' u u' F G l l'}
   (Ru : [Γ ||-<l'> u : F | RF]< wl >)
   (Ru' : [Γ ||-<l'> u' : F | RF]< wl >)
   (Ruu' : [Γ ||-<l'> u ≅ u' : F | RF ]< wl >)
-  (RGu : [Γ ||-<l'> G[u..]]< wl >)
+  (RGu : W[Γ ||-<l'> G[u..]]< wl >)
    :
-    [Γ ||-<l'> tApp t u ≅ tApp t' u' : G[u..] | RGu]< wl >.
+   W[Γ ||-<l'> tApp t u ≅ tApp t' u' : G[u..] | RGu]< wl >.
 Proof.
   set (hΠ := invLRΠ RΠ); pose (RΠ' := LRPi' (normRedΠ0 hΠ)).
-  assert [Γ ||-<l> t ≅ t' : tProd F G | RΠ']< wl > as [Rt Rt' ? eqApp] by irrelevance.
+  assert [Γ ||-<l> t ≅ t' : tProd F G | RΠ']< wl > as [Rt Rt' ?? eqApp] by irrelevance.
   set (h := invLRΠ _) in hΠ.
   epose proof (e := redtywf_whnf (PiRedTyPack.red h) whnf_tProd); 
   symmetry in e; injection e; clear e; 
-  destruct h as [?????? domRed codRed codExt] ; clear RΠ Rtt'; 
+  destruct h as [?????? [?? domRed ? codRed codExt]] ; clear RΠ Rtt'; 
   intros; cbn in *; subst. 
   assert (wfΓ : [|-Γ]< wl >) by gen_typing.
-  assert [Γ ||-<l> u' : F⟨@wk_id Γ⟩ | domRed _ (@wk_id Γ) wfΓ]< wl > by irrelevance.
-  assert [Γ ||-<l> u : F⟨@wk_id Γ⟩ | domRed _ (@wk_id Γ) wfΓ]< wl > by irrelevance.
-  assert (RGu' : [Γ ||-<l> G[u'..]]< wl >).
+  assert [Γ ||-<l> u' : F⟨@wk_id Γ⟩ | domRed _ _ (@wk_id Γ) (idε _) wfΓ]< wl > by irrelevance.
+  assert [Γ ||-<l> u : F⟨@wk_id Γ⟩ | domRed _ _ (@wk_id Γ) (idε _) wfΓ]< wl > by irrelevance.
+  assert (RGu' : W[Γ ||-<l> G[u'..]]< wl >).
   1:{
     replace G[u'..] with G[u' .: @wk_id Γ >> tRel] by now bsimpl.
-    now eapply (codRed _ u' (@wk_id Γ)).
+    exists (posTree _ _ u' (@wk_id Γ) (idε _) wfΓ X).
+    intros wl' f.
+    eapply (codRed _ u' _ (@wk_id Γ) (idε _)).
+    eassumption.
   }
-  assert (RGuu' : [Γ ||-<l>  G [u'..] ≅ G[u..]  | RGu']< wl >).
+  assert (RGuu' : W[Γ ||-<l>  G [u'..] ≅ G[u..]  | RGu']< wl >).
   1:{
     replace G[u..] with G[u .: @wk_id Γ >> tRel] by now bsimpl.
-    irrelevance0.
-    2: unshelve eapply codExt.
-    6: eapply LRTmEqSym; irrelevance.
-    2-4: tea.
-    now bsimpl.
+    unshelve eapply WLRTyEqIrrelevant'.
+    5: exists (posTree _ _ u' (@wk_id Γ) (idε _) wfΓ X) ; intros wl' f Hover.
+    5: irrelevance0 ; [ reflexivity | ].
+    5: unshelve eapply codExt.
+    11: eapply LRTmEqSym; irrelevance.
+    4-8: tea.
+    3: now bsimpl.
+    2: now replace G[u' .: @wk_id Γ >> tRel] with G[u'..] by now bsimpl.
   }
-  eapply transEqTerm; eapply transEqTerm.
-  - eapply (snd (appTerm0 hΠ Rt Ru RGu)).
-  - unshelve epose  proof (eqApp _ u (@wk_id Γ) wfΓ _).  1: irrelevance. 
+  pose (fez:= (snd (appTerm0 hΠ Rt Ru RGu))).
+  pose (zef := (snd (appTerm0 hΠ Rt' Ru' RGu'))).
+  unshelve epose  proof (eqApp _ u _ (@wk_id Γ) (idε _) wfΓ _).  1: irrelevance.
+  cbn in *.
+  eapply WtransEqTerm; eapply WtransEqTerm.
+  - unshelve eapply (snd (appTerm0 hΠ Rt Ru RGu)).
+  - unshelve epose  proof (eqApp _ u _ (@wk_id Γ) (idε _) wfΓ _).  1: irrelevance.
     replace (PiRedTm.nf Rt) with (PiRedTm.nf Rt)⟨@wk_id Γ⟩ by now bsimpl.
-    irrelevance.
-  - unshelve epose proof (PiRedTm.eq Rt' (a:= u) (b:=u') (@wk_id Γ) wfΓ _ _ _).
-    all: irrelevance.
+    unshelve econstructor.
+    2:intros wl' Hover Hover' ; irrelevance0 ; [ | unshelve eapply X2].
+    2: now bsimpl.
+    3: eapply over_tree_fusion_l ; exact Hover'. 
+    eapply over_tree_fusion_r ; exact Hover'.
+  - unshelve epose proof (Hyp := PiRedTm.eq Rt' (a:= u) (b:=u') (@wk_id Γ) (idε wl) wfΓ _ _).
+    3: unshelve econstructor ; [ | intros wl' Hover Hover' ; irrelevance0].
+    5: unshelve eapply Hyp.
+    4: now bsimpl.
+    1,2,5: irrelevance.
+    2: eapply over_tree_fusion_l ; exact Hover'. 
+    eapply over_tree_fusion_r ; exact Hover'.
   - replace (_)⟨_⟩ with (PiRedTm.nf Rt') by now bsimpl.
-    eapply LRTmEqRedConv; tea.
-    eapply LRTmEqSym.
+    eapply WLRTmEqRedConv; tea.
+    eapply WLRTmEqSym.
     eapply (snd (appTerm0 hΠ Rt' Ru' RGu')).
 Qed.
 
-End Application.
 
+Lemma WappcongTerm {wl Γ t t' u u' F G l l'}
+  (RΠ : W[Γ ||-<l> tProd F G]< wl >) 
+  {RF : W[Γ ||-<l'> F]< wl >}
+  (Rtt' : W[Γ ||-<l> t ≅ t' : tProd F G | RΠ]< wl >)
+  (Ru : W[Γ ||-<l'> u : F | RF]< wl >)
+  (Ru' : W[Γ ||-<l'> u' : F | RF]< wl >)
+  (Ruu' : W[Γ ||-<l'> u ≅ u' : F | RF ]< wl >)
+  (RGu : W[Γ ||-<l'> G[u..]]< wl >)
+   :
+   W[Γ ||-<l'> tApp t u ≅ tApp t' u' : G[u..] | RGu]< wl >.
+Proof.
+  revert RGu.
+  pattern wl.
+  unshelve eapply split_to_over_tree.
+  - do 2 (eapply DTree_fusion) ; [eapply DTree_fusion | eapply DTree_fusion | ..].
+    + exact (WT _ RΠ).
+    + exact (WT _ RF).
+    + exact (WTTmEq _ Rtt').
+    + exact (WTTm _ Ru).
+    + exact (WTTm _ Ru').
+    + exact (WTTmEq _ Ruu').
+  - intros wl' n ne Ht Hf RGu.
+    eapply WLRTmEqIrrelevant' ; [reflexivity | unshelve eapply TmEqSplit].
+    2: exact ne.
+    1,2: eapply WLtrans ; [ | eassumption].
+    1,2: eapply LCon_le_step ; now eapply wfLCon_le_id.
+    + now apply Ht.
+    + now apply Hf.
+  - intros wl' Hover RGu.
+    unshelve eapply appcongTerm.
+    3: unshelve eapply (WRed _ RΠ).
+    + now do 3 (eapply over_tree_fusion_l).
+    + eapply (WRed _ RF).
+      now eapply over_tree_fusion_r ; do 2 (eapply over_tree_fusion_l).
+    + eapply (WRedTmEq _ Rtt').
+      now eapply over_tree_fusion_l, over_tree_fusion_r, over_tree_fusion_l.
+    + eapply (WRedTm _ Ru).
+      now eapply over_tree_fusion_r, over_tree_fusion_r, over_tree_fusion_l.
+    + eapply (WRedTm _ Ru').
+      now eapply over_tree_fusion_l, over_tree_fusion_r.
+    + eapply (WRedTmEq _ Ruu').
+      now eapply over_tree_fusion_r, over_tree_fusion_r.
+Qed.
+  
+
+Lemma appcongTerm' {wl Γ t t' u u' F F' G l l' X}
+  (RΠ : [Γ ||-<l> tProd F G]< wl >) 
+  {RF : [Γ ||-<l'> F]< wl >}
+  {RF' : [Γ ||-<l'> F']< wl >}
+  (RFF' : [Γ ||-<l'> F ≅ F' | RF]< wl >)
+  (Rtt' : [Γ ||-<l> t ≅ t' : tProd F G | RΠ]< wl >)
+  (Ru : [Γ ||-<l'> u : F | RF]< wl >)
+  (Ru' : [Γ ||-<l'> u' : F' | RF']< wl >)
+  (Ruu' : [Γ ||-<l'> u ≅ u' : F | RF ]< wl >)
+  (RGu : W[Γ ||-<l'> X]< wl >)
+   : X = G[u..] ->
+    W[Γ ||-<l'> tApp t u ≅ tApp t' u' : X | RGu]< wl >.
+Proof.
+  intros eq.
+  eapply WLRTmEqIrrelevant' ; [symmetry; apply eq|].
+  eapply appcongTerm; tea.
+  eapply LRTmRedConv; tea.
+  now eapply LRTyEqSym.
+  Unshelve. now rewrite <- eq.
+Qed.
 
+Lemma WappcongTerm' {wl Γ t t' u u' F F' G l l' X}
+  (RΠ : W[Γ ||-<l> tProd F G]< wl >) 
+  {RF : W[Γ ||-<l'> F]< wl >}
+  {RF' : W[Γ ||-<l'> F']< wl >}
+  (RFF' : W[Γ ||-<l'> F ≅ F' | RF]< wl >)
+  (Rtt' : W[Γ ||-<l> t ≅ t' : tProd F G | RΠ]< wl >)
+  (Ru : W[Γ ||-<l'> u : F | RF]< wl >)
+  (Ru' : W[Γ ||-<l'> u' : F' | RF']< wl >)
+  (Ruu' : W[Γ ||-<l'> u ≅ u' : F | RF ]< wl >)
+  (RGu : W[Γ ||-<l'> X]< wl >)
+   : X = G[u..] ->
+    W[Γ ||-<l'> tApp t u ≅ tApp t' u' : X | RGu]< wl >.
+Proof.
+  intros eq.
+  eapply WLRTmEqIrrelevant' ; [symmetry; apply eq|].
+  eapply WappcongTerm; tea.
+  eapply WLRTmRedConv ; tea.
+  now eapply WLRTyEqSym.
+  Unshelve. now rewrite <- eq.
+Qed.
+
+End Application.
diff --git a/theories/LogicalRelation/Irrelevance.v b/theories/LogicalRelation/Irrelevance.v
index 9f059ed..a35938e 100644
--- a/theories/LogicalRelation/Irrelevance.v
+++ b/theories/LogicalRelation/Irrelevance.v
@@ -873,6 +873,24 @@ Proof.
   now apply h.
 Defined.
 
+Corollary WLRTransEq@{i j k l} 
+  (wl : wfLCon) (Γ : context) (A B C : term) {lA lB} 
+  (RA : WLogRel@{i j k l} lA wl Γ A)
+  (RB : WLogRel@{i j k l} lB wl Γ B)
+  (RAB : WLogRelEq@{i j k l} lA wl Γ A B RA)
+  (RBC : WLogRelEq@{i j k l} lB wl Γ B C RB) :
+  W[Γ ||-<lA> A ≅ C | RA]< wl >.
+Proof.
+  exists (DTree_fusion _ (DTree_fusion _ (WT _ RB) (WTEq _ RBC)) (WTEq _ RAB)).
+  intros wl' Hover Hover'.
+  eapply LRTransEq.
+  - unshelve eapply (WRedEq _ RAB).
+    now eapply over_tree_fusion_r.
+  - unshelve eapply (WRedEq _ RBC).
+    + now eapply over_tree_fusion_l, over_tree_fusion_l.
+    + now eapply over_tree_fusion_r, over_tree_fusion_l.
+Defined.
+
 
 Theorem LRCumulative@{i j k l i' j' k' l'} {lA}
   {wl : wfLCon} {Γ : context} {A : term}
@@ -922,6 +940,20 @@ Proof.
   revert lrA'; rewrite <- e; now apply LRTyEqIrrelevantCum.
 Qed.
 
+Corollary WLRTyEqIrrelevant'@{i j k l} lA lA' wl Γ A A' (e : A = A')
+  (lrA : WLogRel@{i j k l} lA wl Γ A) (lrA' :WLogRel@{i j k l} lA' wl Γ A') :
+  forall B, W[Γ ||-< lA > A ≅ B | lrA]< wl > -> W[Γ ||-< lA' > A' ≅ B | lrA']< wl >.
+Proof.
+  intros B [] ; unshelve econstructor.
+  - eapply DTree_fusion.
+    + exact WTEq.
+    + exact (WT _ lrA).
+  - intros wl' Hover Hover' ; eapply LRTyEqIrrelevant' ; [eassumption | ].
+    unshelve eapply WRedEq.
+    + now eapply over_tree_fusion_r.
+    + now eapply over_tree_fusion_l.
+Qed.
+
 #[local]
 Corollary RedTmIrrelevantCum wl Γ A {lA eqTyA redTmA eqTmA lA' eqTyA' redTmA' eqTmA'}
   (lrA : LogRel lA wl Γ A eqTyA redTmA eqTmA) (lrA' : LogRel lA' wl Γ A eqTyA' redTmA' eqTmA') :
@@ -954,6 +986,20 @@ Proof.
   revert lrA'; rewrite <- e; now apply LRTmRedIrrelevantCum.
 Qed.
 
+Corollary WLRTmRedIrrelevant'@{i j k l} lA lA' wl Γ A A' (e : A = A')
+  (lrA : WLogRel@{i j k l} lA wl Γ A) (lrA' :WLogRel@{i j k l} lA' wl Γ A') :
+  forall t, W[Γ ||-< lA > t : A | lrA]< wl > -> W[Γ ||-< lA' > t : A' | lrA']< wl >.
+Proof.
+  intros t [] ; unshelve econstructor.
+  - eapply DTree_fusion.
+    + exact WTTm.
+    + exact (WT _ lrA).
+  - intros wl' Hover Hover' ; eapply LRTmRedIrrelevant' ; [eassumption | ].
+    unshelve eapply WRedTm.
+    + now eapply over_tree_fusion_r.
+    + now eapply over_tree_fusion_l.
+Qed.
+
 
 #[local]
 Corollary TmEqIrrelevantCum wl Γ A {lA eqTyA redTmA eqTmA lA' eqTyA' redTmA' eqTmA'}
@@ -987,6 +1033,19 @@ Proof.
   revert lrA'; rewrite <- e; now apply LRTmEqIrrelevantCum.
 Qed.
 
+Corollary WLRTmEqIrrelevant'@{i j k l} lA lA' wl Γ A A' (e : A = A')
+  (lrA : WLogRel@{i j k l} lA wl Γ A) (lrA' :WLogRel@{i j k l} lA' wl Γ A') :
+  forall t u, W[Γ ||-< lA > t ≅ u : A | lrA]< wl > -> W[Γ ||-< lA' > t ≅ u : A' | lrA']< wl >.
+Proof.
+  intros t u [] ; unshelve econstructor.
+  - eapply DTree_fusion.
+    + exact WTTmEq.
+    + exact (WT _ lrA).
+  - intros wl' Hover Hover' ; eapply LRTmEqIrrelevant' ; [eassumption | ].
+    unshelve eapply WRedTmEq.
+    + now eapply over_tree_fusion_r.
+    + now eapply over_tree_fusion_l.
+Qed.
 
 
 Corollary TyEqSym wl Γ A A' {lA eqTyA redTmA eqTmA lA' eqTyA' redTmA' eqTmA'}
@@ -1007,6 +1066,18 @@ Proof.
   now eapply TyEqSym.
 Qed.
 
+Corollary WLRTyEqSym lA lA' wl Γ A A' (lrA : W[Γ ||-< lA > A]< wl >) (lrA' : W[Γ ||-< lA'> A']< wl >) :
+  W[Γ ||-< lA > A ≅ A' | lrA]< wl > -> W[Γ ||-< lA' > A' ≅ A | lrA']< wl >.
+Proof.
+  destruct lrA as [d Hd], lrA' as [d' Hd'].
+  intros [deq Hdeq] ; cbn in *.
+  exists (DTree_fusion _ d deq).
+  intros wl' Hover Hover' ; eapply LRTyEqSym.
+  unshelve eapply Hdeq.
+  - now eapply over_tree_fusion_l.
+  - now eapply over_tree_fusion_r.
+Qed.
+
 #[local]
 Corollary RedTmConv wl Γ A A' {lA eqTyA redTmA eqTmA lA' eqTyA' redTmA' eqTmA'}
   (lrA : LogRel lA wl Γ A eqTyA redTmA eqTmA) (lrA' : LogRel lA' wl Γ A' eqTyA' redTmA' eqTmA') :
@@ -1025,6 +1096,21 @@ Proof.
   now eapply RedTmConv.
 Qed.
 
+Corollary WLRTmRedConv lA lA' wl Γ A A' (lrA : W[Γ ||-< lA > A]< wl >) (lrA' : W[Γ ||-< lA'> A' ]< wl >) :
+  W[Γ ||-< lA > A ≅ A' | lrA ]< wl > ->
+  forall t, W[Γ ||-< lA > t : A | lrA]< wl > -> W[Γ ||-< lA' > t : A' | lrA']< wl >.
+Proof.
+  destruct lrA as [d Hd], lrA' as [d' Hd'].
+  intros [deq Hdeq] t [deqt Hdeqt] ; cbn in *.
+  exists (DTree_fusion _ (DTree_fusion _ d deq) deqt).
+  intros wl' Hover Hover' ; eapply LRTmRedConv.
+  - cbn in *. unshelve eapply Hdeq.
+    + now do 2 (eapply over_tree_fusion_l).
+    + now eapply over_tree_fusion_r, over_tree_fusion_l.
+  - eapply Hdeqt.
+    now eapply over_tree_fusion_r.
+Qed.
+
 Corollary PolyRedEqSym {wl Γ l l' shp shp' pos pos'}
   {PA : PolyRed wl Γ l shp pos}
   (PA' : PolyRed wl Γ l' shp' pos') :
@@ -1068,6 +1154,25 @@ Proof.
   now eapply TmEqRedConv.
 Qed.
 
+Corollary WLRTmEqRedConv lA lA' wl Γ A A' (lrA : W[Γ ||-< lA > A]< wl >) (lrA' : W[Γ ||-< lA'> A']< wl >) :
+  W[Γ ||-< lA > A ≅ A' | lrA ]< wl > ->
+  forall t u, W[Γ ||-< lA > t ≅ u : A | lrA]< wl > -> W[Γ ||-< lA' > t ≅ u : A' | lrA']< wl >.
+Proof.
+  destruct lrA, lrA' ; intros [WEq WRedEq] t u [WTmEq WRedTmEq].
+  unshelve econstructor.
+  + eapply DTree_fusion ; [eapply DTree_fusion | ].
+    * exact WEq.
+    * exact WT.
+    * exact WTmEq.
+  + intros wl' Hover Hover' ; cbn in *.
+    eapply LRTmEqRedConv.
+    2: unshelve eapply WRedTmEq.
+    eapply WRedEq.
+    * now do 2 (eapply over_tree_fusion_l).
+    * now eapply over_tree_fusion_r, over_tree_fusion_l.
+    * now eapply over_tree_fusion_r.
+Qed.
+
 Corollary LRTmTmEqIrrelevant' lA lA' wl Γ A A' (e : A = A')
   (lrA : [Γ ||-< lA > A]< wl >) (lrA' : [Γ ||-< lA'> A']< wl >) :
   forall t u, 
@@ -1136,6 +1241,13 @@ Proof.
     now eapply NeNfEqSym.    
 Qed.
 
+Lemma WLRTmEqSym@{h i j k l} lA wl Γ A (lrA : WLogRel@{i j k l} lA wl Γ A) : forall t u,
+    W[Γ ||-<lA> t ≅ u : A |lrA]< wl > -> W[Γ ||-<lA> u ≅ t : A |lrA]< wl >.
+Proof.
+  intros t u [d Hd] ; exists d.
+  intros wl' Hover Hover' ; now eapply LRTmEqSym.
+Qed.
+
 End Irrelevances.
 
 
diff --git a/theories/LogicalRelation/Monotonicity.v b/theories/LogicalRelation/Monotonicity.v
index 0d2f68b..71b2623 100644
--- a/theories/LogicalRelation/Monotonicity.v
+++ b/theories/LogicalRelation/Monotonicity.v
@@ -1,127 +1,742 @@
-(** * LogRel.LogicalRelation.Escape: the logical relation implies conversion/typing. *)
-Require Import PeanoNat Nat.
-From Coq Require Import CRelationClasses.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations LContexts Context NormalForms GenericTyping LogicalRelation DeclarativeInstance.
-From LogRel.LogicalRelation Require Import Induction.
+From LogRel Require Import Notations Utils BasicAst LContexts Context NormalForms UntypedValues Weakening GenericTyping Monad LogicalRelation DeclarativeInstance.
+From LogRel.LogicalRelation Require Import Induction Irrelevance Reflexivity Transitivity Escape Weakening.
 
 Set Universe Polymorphism.
 
-Section Monotonicity.
+Section Red_Ltrans.
   Context `{GenericTypingProperties}.
+  
+Lemma Id_Ltrans@{h i j k l} (l : TypeLevel) (wl : wfLCon) (Γ : context) (A : term)
+  (IA : IdRedTy@{i j k l} wl Γ l A)
+  (ih1 : forall wl' : wfLCon,
+      wl' ≤ε wl -> [LogRel@{i j k l} l | Γ ||- IdRedTy.ty@{i j k l} IA ]< wl' >)
+  (ih2 : forall (Δ : context) (wl' : wfLCon) (ρ : Δ ≤ Γ),
+      wl' ≤ε wl -> [ |-[ ta ] Δ ]< wl' > ->
+      forall wl'' : wfLCon,
+        wl'' ≤ε wl' ->
+        [LogRel@{i j k l} l | Δ ||- (IdRedTy.ty@{i j k l} IA)⟨ρ⟩ ]< wl'' >)
+  (wl' : wfLCon)
+  (f : wl' ≤ε wl)
+  (Hg : [ |-[ ta ] Γ ]< wl >) : IdRedTy@{i j k l} wl' Γ l A.
+Proof.
+  unshelve econstructor.
+  6: econstructor ; [eapply wft_Ltrans, (IdRedTy.red IA).(tyr_wf_r _ _ _ _) ; eauto |
+                      eapply redty_Ltrans ; eauto].
+  3: now eapply (IdRedTy.red IA).(tyr_wf_red _ _ _ _).
+  3: eapply convty_Ltrans ; eauto ; now eapply (IdRedTy.eq IA).
+  + now eapply ih1.
+  + intros * f' Hd ; eapply ih2 ; [ | eassumption | now eapply wfLCon_le_id].
+    now eapply wfLCon_le_trans.
+  + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+    destruct (wk_id_ren_on Γ  (IdRedTy.lhs IA)). 
+    eapply (IdRedTy.tyKripkeTm IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
+    * now bsimpl.
+    * irrelevance0 ; [symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+      now eapply (IdRedTy.lhsRed).
+  + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+    destruct (wk_id_ren_on Γ  (IdRedTy.rhs IA)).
+    eapply (IdRedTy.tyKripkeTm IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
+    * now bsimpl.
+    * irrelevance0 ; [symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+      now eapply (IdRedTy.rhsRed).
+  + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+    destruct (wk_id_ren_on Γ  (IdRedTy.lhs IA)).
+    eapply (IdRedTy.tyKripkeTmEq IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
+    * now bsimpl.
+    * irrelevance0 ; [symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+      now eapply (IdRedTy.lhsRedRefl).
+  + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+    destruct (wk_id_ren_on Γ  (IdRedTy.rhs IA)).
+    eapply (IdRedTy.tyKripkeTmEq IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
+    * now bsimpl.
+    * irrelevance0 ; [symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+      now eapply (IdRedTy.rhsRedRefl).
+  + econstructor.
+    * intros ??? ; eapply (LREqTermSymConv); [eassumption | ].
+      now eapply reflLRTyEq.
+    * intros ????? ; eapply (transEqTerm@{h i j k l}) ; eassumption.
+  + intros ?? wl'' wl''' ??? f' f'' ??? Heq Hyp.
+    irrelevance0 ; [reflexivity | ].
+    eapply (IdRedTy.tyKripkeEq IA _ _ _ (f' •ε f) f'' wfΔ wfΞ _ Heq).
+    irrelevance0 ; [ reflexivity | eassumption].
+  + intros ?? wl'' wl''' ??? f' f'' ??? Heq Hyp.
+    irrelevance0 ; [reflexivity | ].
+    eapply (IdRedTy.tyKripkeTm IA _ _ _ (f' •ε f) f'' wfΔ wfΞ _ Heq).
+    irrelevance0 ; [ reflexivity | eassumption].
+  + intros ?? wl'' wl''' ??? f' f'' ???? Heq Hyp.
+    irrelevance0 ; [reflexivity | ].
+    eapply (IdRedTy.tyKripkeTmEq IA _ _ _ (f' •ε f) f'' wfΔ wfΞ _ _ Heq).
+    irrelevance0 ; [ reflexivity | eassumption].
+Defined.
+
+  Lemma Ltrans@{h i j k l} {wl Γ wl' A l} :
+    (wl' ≤ε wl) ->
+    [LogRel@{i j k l} l | Γ ||- A]< wl > ->
+    [LogRel@{i j k l} l | Γ ||- A]< wl' >.
+  Proof.
+    intros f lrA. revert wl' f. pattern l, wl, Γ, A, lrA.
+    eapply LR_rect_TyUr@{i j k l l}; clear l wl Γ A lrA.
+    - intros * [??? []] ??. apply LRU_.
+      econstructor ; eauto ; [now eapply wfc_Ltrans | econstructor ].
+      + now eapply wft_Ltrans.
+      + now eapply redty_Ltrans.
+    - intros ????[ty[]]??. apply LRne_ ; econstructor ; [econstructor | ].
+      + now eapply wft_Ltrans.
+      + now eapply redty_Ltrans.
+      + now eapply convneu_Ltrans.
+    - intros ???? [] ihdom ihcod wl' f ; cbn in *.
+      apply LRPi' ; econstructor ; [destruct red ; econstructor |..].
+      + now eapply wft_Ltrans.
+      + now eapply redty_Ltrans.
+      + now eapply convty_Ltrans.
+      + now eapply convty_Ltrans.
+      + unshelve econstructor.
+        4,5: destruct polyRed ; now eapply wft_Ltrans.
+        * intros * f' Hd.
+          eapply (PolyRed.shpRed polyRed) ; [eapply wfLCon_le_trans | ] ; eauto.
+        * intros ???? f' Hd ha ; cbn in *.
+          eapply (PolyRed.posTree polyRed) ; eauto.
+        * intros ???? f' ??? Hover ; cbn in *.
+          eapply (PolyRed.posRed polyRed) ; eassumption.
+        * intros ???? f' ????? Hover Hover' ; cbn in *.
+          eapply (PolyRed.posExt polyRed) ; eassumption.
+    - intros ????? wl' f.
+      eapply LRNat_ ; econstructor.
+      eapply redtywf_Ltrans ; eauto.
+      now eapply NA.(NatRedTy.red).
+    - intros ????? wl' f.
+      eapply LRBool_ ; econstructor.
+      eapply redtywf_Ltrans ; eauto.
+      now eapply NA.(BoolRedTy.red).
+    - intros ????? wl' f.
+      eapply LREmpty_ ; econstructor.
+      eapply redtywf_Ltrans ; eauto.
+      now eapply NA.(EmptyRedTy.red).
+    - intros ???? [] ihdom ihcod wl' f ; cbn in *.
+      apply (LRSig'@{i j k l}) ; econstructor ; [destruct red ; econstructor |..].
+      + now eapply wft_Ltrans.
+      + now eapply redty_Ltrans.
+      + now eapply convty_Ltrans.
+      + now eapply convty_Ltrans.
+      + unshelve econstructor.
+        4,5: destruct polyRed ; now eapply wft_Ltrans.
+        * intros * f' Hd.
+          eapply (PolyRed.shpRed polyRed) ; [eapply wfLCon_le_trans | ] ; eauto.
+        * intros ???? f' Hd ha ; cbn in *.
+          eapply (PolyRed.posTree polyRed) ; eauto.
+        * intros ???? f' ??? Hover ; cbn in *.
+          eapply (PolyRed.posRed polyRed) ; eassumption.
+        * intros ???? f' ????? Hover Hover' ; cbn in *.
+          eapply (PolyRed.posExt polyRed) ; eassumption.
+    - intros ????? ih1 ih2 wl' f. 
+      apply (LRId'@{i j k l}).
+      eapply (Id_Ltrans@{h i j k l}) ; eauto.
+      now eapply (wfc_convty (IdRedTy.eq IA)).
+  Defined.
 
-Lemma LRTy_Ltrans@{i i' j j' k k' l l'} {lA} (wl wl' : wfLCon) (f : wl' ≤ε wl)
-    (Γ : context) (A : term) :
-    [ LogRel@{i j k l} lA | Γ ||- A ]< wl > ->
-    [ LogRel@{i j k l} lA | Γ ||- A ]< wl' >.
+  Lemma WLtrans@{h i j k l} {wl Γ wl' A l} :
+    (wl' ≤ε wl) ->
+    WLogRel@{i j k l} l wl Γ A  ->
+    WLogRel@{i j k l} l wl' Γ A.
+  Proof.
+    intros f HA ; unshelve econstructor.
+    - eapply DTree_Ltrans ; [eassumption | ].
+      exact (WT _ HA).
+    - intros wl'' Hover.
+      eapply (WRed _ HA).
+      now eapply over_tree_Ltrans.
+  Defined.      
+
+  
+Lemma Eq_Ltrans@{h i j k l} {wl Γ wl' A B l} (f : wl' ≤ε wl) (lrA : [Γ ||-<l> A]< wl >) : 
+    [LogRel@{i j k l} l | Γ ||- A ≅ B | lrA]< wl > ->
+    [LogRel@{i j k l} l | Γ ||- A ≅ B | Ltrans@{h i j k l} f lrA]< wl' >.
 Proof.
-  intros [ [] lrA ] ; cbn in lrA.
-  induction lrA as [? ? ? [l1 lt1] | ? ? ? [] | ? ? ? [] [] IHdom IHcod|??? []|??? [] |??? []] ; intros.
-  - unshelve eapply LRU_.
-    unshelve econstructor ; try assumption.
-    + now eapply wfc_Ltrans.
-    + destruct red.
-      split ; try now eapply redty_Ltrans.
-      now eapply wft_Ltrans.
-  - unshelve eapply LRne_.
-    unshelve econstructor ; try assumption.
-    + destruct red ; split ; try now eapply redty_Ltrans.
-      now eapply wft_Ltrans.
-    + now eapply ty_ne_Ltrans.
+  revert B wl' f. pattern l, wl, Γ, A, lrA.
+  eapply LR_rect_TyUr@{i j k l l}; clear l wl Γ A lrA.
+  - intros ???? [??? []] ???[] ; cbn in *.
+    constructor ; constructor.
+    + now eapply wft_Ltrans.
+    + destruct red ; now eapply redty_Ltrans.
+  - intros ???? [?[]] ???[?[]] ; cbn in *.
+    econstructor ; [econstructor | ].
+    + now eapply wft_Ltrans.
+    + now eapply redty_Ltrans.
     + now eapply convneu_Ltrans.
-  - unshelve eapply LRPi_.
+  - intros ???? [] ihdom ihcod B wl' f []; cbn in *.
+    econstructor ; [destruct red0 ; econstructor |..].
+    + now eapply wft_Ltrans.
+    + now eapply redty_Ltrans.
+    + now eapply convty_Ltrans.
+    + now eapply convty_Ltrans.
+    + unshelve econstructor ; cbn in *.
+      * intros * ? ; now eapply (PolyRedEq.posTree polyRed0).
+      * intros * ; now eapply (PolyRedEq.shpRed polyRed0).
+      * cbn ; intros * Ho' ; now eapply (PolyRedEq.posRed polyRed0).
+  - intros ???? [[]] B wl' f [[]] ; cbn in *.
+    econstructor ; econstructor.
+    + now eapply wft_Ltrans.
+    + now eapply redty_Ltrans.
+  - intros ???? [[]] B wl' f [[]] ; cbn in *.
+    econstructor ; econstructor.
+    + now eapply wft_Ltrans.
+    + now eapply redty_Ltrans.
+  - intros ???? [[]] B wl' f [[]] ; cbn in *.
+    econstructor ; econstructor.
+    + now eapply wft_Ltrans.
+    + now eapply redty_Ltrans.
+  - intros ???? [] ihdom ihcod B wl' f [] ; cbn in *.
+    econstructor ; [destruct red0 ; econstructor | ..].
+    + now eapply wft_Ltrans.
+    + now eapply redty_Ltrans.
+    + now eapply convty_Ltrans.
+    + now eapply convty_Ltrans.
+    + unshelve econstructor ; cbn.
+      * intros * ? ; now eapply (PolyRedEq.posTree polyRed0).
+      * intros * ; now eapply (PolyRedEq.shpRed polyRed0).
+      * cbn ; intros * Ho' ; now eapply (PolyRedEq.posRed polyRed0).
+  - intros ????? ih1 ih2 ????.
+    assert (Hg:= (wfc_convty (IdRedTy.eq IA))).
+    eapply (@Build_IdRedTyEq _ _ _ _ _ _ wl' Γ A _ B) ; cbn.
+    + unshelve econstructor.
+      * now eapply wft_Ltrans, (IdRedTyEq.red X).(tyr_wf_r _ _ _ _).
+      * now eapply redty_Ltrans, (IdRedTyEq.red X).(tyr_wf_red _ _ _ _).
+    + eapply convty_Ltrans ; [ eassumption | ].
+      eapply (IdRedTyEq.eq X). 
+    + eapply ih1.
+      now eapply (IdRedTyEq.tyRed X).
+    + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+      destruct (wk_id_ren_on Γ  (IdRedTy.lhs IA)).
+      destruct (wk_id_ren_on Γ  (IdRedTyEq.lhs X)).
+      eapply (IdRedTy.tyKripkeTmEq IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
+      * now bsimpl.
+      * irrelevance0 ; [ symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+        exact (IdRedTyEq.lhsRed X).
+    + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+      destruct (wk_id_ren_on Γ  (IdRedTy.rhs IA)).
+      destruct (wk_id_ren_on Γ  (IdRedTyEq.rhs X)).
+      eapply (IdRedTy.tyKripkeTmEq IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
+      * now bsimpl.
+      * irrelevance0 ; [ symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
+        exact (IdRedTyEq.rhsRed X).
+Qed.
+
+  Lemma WEq_Ltrans@{h i j k l} {wl Γ wl' A B l}
+    (f : wl' ≤ε wl) (lrA : W[Γ ||-<l> A]< wl >) :
+    WLogRelEq@{i j k l} l wl Γ A B lrA ->
+    WLogRelEq@{i j k l} l wl' Γ A B (WLtrans@{h i j k l} f lrA).
+  Proof.
+    intros Heq ; unshelve econstructor.
+    - eapply DTree_Ltrans ; [eassumption | ].
+      exact (WTEq _ Heq).
+    - intros wl'' Hover Hover'.
+      eapply (WRedEq _ Heq).
+      now eapply over_tree_Ltrans.
+  Defined.      
+
+
+
+Lemma isLRFun_Ltrans : forall wl wl' Γ t A l (f : wl' ≤ε wl) (ΠA : [Γ ||-Π< l > A]< wl >)
+                              (ΠA' : [Γ ||-Π< l > A]< wl' >),
+    isLRFun ΠA t -> isLRFun ΠA' t.
+Proof.
+  intros * f * Hyp.
+  unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)).
+  1,2: now econstructor.
+  inversion Heq.
+  induction Hyp as [?? funTree e r | t Heqt].
+  - unshelve econstructor.
+    + intros Δ wl'' a ρ f' Hd ha ; cbn.
+      eapply DTree_fusion.
+      * unshelve eapply funTree.
+        6: irrelevance0 ; [ | exact ha] ; now f_equal.
+        2: assumption.
+        now eapply wfLCon_le_trans.
+      * unshelve eapply (PolyRedPack.posTree ΠA).
+        5: eassumption.
+        4: irrelevance0 ; [ | exact ha] ; now f_equal.
+        now eapply wfLCon_le_trans.
+    + intros Δ wl'' ρ f' Hd ; cbn.
+      irrelevance0 ; [ | unshelve eapply e] ; [now f_equal | ..].
+      2: assumption.
+      now eapply wfLCon_le_trans.
+    + intros Δ wl'' a ρ f' Hd ha wl''' Ho Ho'.
+      irrelevance0 ; [ | unshelve eapply r].
+      now f_equal.
+      3: eassumption.
+      now eapply wfLCon_le_trans.
+      cbn in *.
+      3: now eapply over_tree_fusion_l.
+      now eapply over_tree_fusion_r.
+  - econstructor 2.
     cbn in *.
-    unshelve econstructor.
-    + exact dom.
-    + exact cod.
-    + exact domN.
-    + intros.
-      unshelve eapply domRed ; try assumption.
+    rewrite <- H11, <- H12.
+    now eapply convneu_Ltrans.
+Qed.
+
+Lemma isLRPair_Ltrans : forall wl wl' Γ t A l (f : wl' ≤ε wl) (ΣA : [Γ ||-Σ< l > A]< wl >)
+                              (ΣA' : [Γ ||-Σ< l > A]< wl' >),
+    isLRPair ΣA t -> isLRPair ΣA' t.
+Proof.
+  intros * f * Hyp.
+  unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΣA.(ParamRedTyPack.red)) ΣA'.(ParamRedTyPack.red)).
+  1,2: now econstructor.
+  inversion Heq.
+  induction Hyp as [????? fstTree ?? sndTree | t Heqt].
+  - unshelve econstructor.
+    + intros Δ wl'' a' ρ f' Hd ha ; cbn.
+      eapply DTree_fusion.
+      * unshelve eapply fstTree.
+        6: irrelevance0 ; [ | exact ha] ; now f_equal.
+        2: assumption.
+        now eapply wfLCon_le_trans.
+      * unshelve eapply (PolyRedPack.posTree ΣA).
+        5: eassumption.
+        4: irrelevance0 ; [ | exact ha] ; now f_equal.
+        now eapply wfLCon_le_trans.
+    + intros Δ wl'' ρ f' Hd ; cbn.
+      irrelevance0 ; [ | unshelve eapply rfst] ; [now f_equal | ..].
+      2: assumption.
       now eapply wfLCon_le_trans.
-    + intros.
-      unshelve eapply codomN ; try assumption.
+    + intros Δ wl'' ρ f' Hd.
+      eapply DTree_fusion.
+      * eapply sndTree.
+        1,3: eassumption.
+        now eapply wfLCon_le_trans.
+      * unshelve  eapply (PolyRed.posTree ΣA).
+        6: now unshelve eapply rfst.
+        2,4: eassumption.
+        now eapply wfLCon_le_trans.
+    + intros Δ wl'' ρ f' Hd.
+      irrelevance0 ; [ | unshelve eapply rdom ; eauto].
+      now f_equal.
       now eapply wfLCon_le_trans.
-      assumption.
-    + intros ; cbn in *.
-      unshelve eapply codRed ; [ exact l' | ..] ; try assumption.
+    + intros Δ wl'' a' ρ f' Hd ha wl''' Ho Ho' ; cbn in *.
+      irrelevance0 ; [ | unshelve eapply rcod].
+      1: now f_equal.
+      3: eassumption.
       * now eapply wfLCon_le_trans.
+      * irrelevance0 ; [ | exact ha] ; now f_equal.
+      * cbn in * ; now eapply over_tree_fusion_r.
+      * cbn in * ; now eapply over_tree_fusion_l.
+    + intros Δ wl'' ρ f' Hd wl''' Ho Ho' ; cbn in *.
+      irrelevance0 ; [ | unshelve eapply rsnd].
+      1: now f_equal.
+      3: eassumption.
+      * now eapply wfLCon_le_trans.
+      * cbn in * ; now eapply over_tree_fusion_r.
+      * cbn in * ; now eapply over_tree_fusion_l.
+  - econstructor 2.
+    cbn in *.
+    rewrite <- H11, <- H12.
+    now eapply convneu_Ltrans.
+Qed.
+
+Lemma NatTm_Ltrans (l : TypeLevel) (wl : wfLCon) (Γ : context) (A : term)
+  (NA : [Γ ||-Nat A ]< wl >) (t : term) (wl' : wfLCon) (f : wl' ≤ε wl) (NA' : [Γ ||-Nat A ]< wl' >) :
+  [LRNat_ l NA | Γ ||- t : A ]< wl > -> [ (LRNat_ l NA') | Γ ||- t : A ]< wl' >.
+Proof.
+  revert t.
+  set (G := _); enough (h : G × (forall t, NatProp NA t -> NatProp NA' t)) by apply h.
+  subst G; apply NatRedInduction.
+  - intros t nf Hred Heq Hprop Hprop'.
+    econstructor ; [now eapply redtmwf_Ltrans | | ].
+    + now eapply convtm_Ltrans.
+    + assumption.
+  - now econstructor.
+  - intros n Hn Hn' ; now econstructor.
+  - intros ; econstructor.
+    destruct r ; econstructor.
+    + now eapply ty_Ltrans.
+    + now eapply convneu_Ltrans.
+Qed.
+
+Lemma IdTm_Ltrans (l : TypeLevel) (wl wl' : wfLCon) (Γ : context) (A : term) (f : wl' ≤ε wl)
+  (IA : [Γ ||-Id< l > A ]< wl >) (IA' : [Γ ||-Id< l > A ]< wl' >)
+  (ih1 : forall (t : term),
+      [IdRedTy.tyRed IA | Γ ||- t : IdRedTy.ty IA ]< wl > ->
+      [IdRedTy.tyRed IA' | Γ ||- t : IdRedTy.ty IA' ]< wl' >)
+  (ih2 : forall (Δ : context) (ρ : Δ ≤ Γ) (wfΔ : [ |-[ ta ] Δ ]< wl' >)
+                (t : term) (wl'' : wfLCon) (f' : wl'' ≤ε wl'),
+      [IdRedTy.tyKripke IA ρ f wfΔ | Δ ||- t : (IdRedTy.ty IA)⟨ρ⟩ ]< wl' > ->
+      [IdRedTy.tyKripke IA' ρ f' (wfc_Ltrans f' wfΔ) | Δ ||- t : (IdRedTy.ty IA')⟨ρ⟩ ]< wl'' >) :
+      forall (t : term),
+        [LRId' IA | Γ ||- t : A ]< wl > -> [LRId' IA' | Γ ||- t : A ]< wl' >.
+Proof.
+  intros t Ht.
+  unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f (IdRedTy.red IA))
+                           (IdRedTy.red IA')).
+  1,2 : now econstructor.
+  inversion Heq.
+  assert (Hg:= (wfc_convty (IdRedTy.eq IA))).
+  econstructor ; cbn.
+  - cbv in H11,H12,H13 ; cbv. 
+    rewrite <- H11, <- H12, <- H13.
+    now eapply redtmwf_Ltrans ; [ | eapply (IdRedTm.red Ht)].
+  - cbv in H11,H12,H13 ; cbv. 
+    rewrite <- H11, <- H12, <- H13.
+    now eapply convtm_Ltrans ; [ | eapply (IdRedTm.eq Ht)].
+  - destruct (IdRedTm.prop Ht).
+    + econstructor.
+      * now eapply wft_Ltrans.
+      * now eapply ty_Ltrans.
+      * irrelevance0 ; [ | unshelve eapply Eq_Ltrans].
+        5: eassumption.
+        all: assumption.
+      * assert (Help : IdRedTyPack.lhs (IdRedTy.toPack IA') = IdRedTyPack.lhs (IdRedTy.toPack IA)).
+        { now eauto. }
+        rewrite Help.
+        irrelevance0.
+        2:{ erewrite <- (wk_id_ren_on Γ (IdRedTyPack.lhs (IdRedTy.toPack IA))).
+            erewrite <- wk_id_ren_on.
+            eapply (IdRedTy.tyKripkeTmEq IA wk_id wk_id _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
+            * now bsimpl.
+            * irrelevance0 ; [rewrite wk_id_ren_on ; reflexivity | ].
+              eassumption.
+        }
+        rewrite H11 ; bsimpl.
+        reflexivity.
+      * assert (Help : IdRedTyPack.rhs (IdRedTy.toPack IA') = IdRedTyPack.rhs (IdRedTy.toPack IA)).
+        { now eauto. }
+        rewrite Help.
+        irrelevance0.
+        2:{ erewrite <- (wk_id_ren_on Γ (IdRedTyPack.rhs (IdRedTy.toPack IA))).
+            erewrite <- wk_id_ren_on.
+            eapply (IdRedTy.tyKripkeTmEq IA wk_id wk_id _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
+            * now bsimpl.
+            * irrelevance0 ; [rewrite wk_id_ren_on ; reflexivity | ].
+              eassumption.
+        }
+        rewrite H11 ; bsimpl.
+        reflexivity.
+    + econstructor.
+      destruct r ; econstructor.
+      * eapply ty_Ltrans ; [eassumption | ].
+        assert (Help : IdRedTyPack.outTy (IdRedTy.toPack IA') = IdRedTyPack.outTy (IdRedTy.toPack IA)) by eauto.
+        now rewrite Help.
+      * eapply convneu_Ltrans ; [eassumption | ].
+        assert (Help : IdRedTyPack.outTy (IdRedTy.toPack IA') = IdRedTyPack.outTy (IdRedTy.toPack IA)) by eauto.
+        now rewrite Help.
+Qed.
+
+Lemma ΠTm_Ltrans (l : TypeLevel) (wl wl' : wfLCon) (Γ : context) (f : wl' ≤ε wl) (A : term)
+  (ΠA : [Γ ||-Π< l > A ]< wl >)
+  (ΠA' : [Γ ||-Π< l > A ]< wl' >)
+  (ihdom : forall (Δ : context) (ρ : Δ ≤ Γ) (h : [ |-[ ta ] Δ ]< wl' >) (t : term)
+                  (wl'' : wfLCon) (f' : wl'' ≤ε wl'),
+      [PolyRed.shpRed ΠA ρ f h | Δ ||- t : (ParamRedTy.dom ΠA)⟨ρ⟩ ]< wl' > ->
+      [Ltrans f' (PolyRed.shpRed ΠA ρ f h) | Δ ||- t : (ParamRedTy.dom ΠA)⟨ρ⟩ ]< wl'' >)
+  (ihcod : forall (Δ : context) (a : term) (ρ : Δ ≤ Γ) (h : [ |-[ ta ] Δ ]< wl' >)
+                  (ha : [PolyRed.shpRed ΠA ρ f h | Δ ||- a : (ParamRedTy.dom ΠA)⟨ρ⟩ ]< wl' >)
+                  (wl'' : wfLCon) (Ho : over_tree wl' wl'' (PolyRed.posTree ΠA ρ f h ha))
+                  (t : term) (wl''' : wfLCon) (f'' : wl''' ≤ε wl''),
+      [PolyRed.posRed ΠA ρ f h ha Ho | Δ  ||- t : (ParamRedTy.cod ΠA)[a .: ρ >> tRel] ]< wl'' > ->
+      [Ltrans f'' (PolyRed.posRed ΠA ρ f h ha Ho) | Δ  ||- t : (ParamRedTy.cod ΠA)[a .: ρ >> tRel] ]< wl''' >) :
+  forall (t : term),
+    [Γ ||-Π t : A | ΠA ]< wl > ->  [Γ ||-Π t : A | ΠA' ]< wl' >.
+Proof.
+  intros t [].
+  unshelve econstructor ; [ | | eapply redtmwf_Ltrans ; eauto |..].
+  1: exact nf.
+  1:{ cbn in * ; intros.
+      eapply DTree_fusion.
+      * unshelve eapply appTree.
+        4: eapply wfLCon_le_trans.
+        3-6: eassumption.
+        2: irrelevance0 ; [ | eassumption ].
+        f_equal.
+        unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)) ; [now econstructor | now econstructor | ].
+        now inversion Heq.
+    * eapply (PolyRed.posTree ΠA ρ (f0 •ε f) Hd).
+      irrelevance0 ; [ | eassumption].
+      f_equal.
+      unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)) ; [now econstructor | now econstructor | ].
+      now inversion Heq.
+  }
+  all: unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)) ; [now econstructor | now econstructor | ].
+  all: inversion Heq.
+  2: eapply convtm_Ltrans ; [eauto | now rewrite <- Heq].
+  2: eapply isLRFun_Ltrans ; eauto.
+  1: now rewrite <- Heq.
+  + cbn in * ; intros. 
+    irrelevance0 ; [ | unshelve eapply app].
+    6: now eapply over_tree_fusion_r.
+    * now f_equal.
+    * now eapply over_tree_fusion_l.
+  + cbn in * ; intros.
+    irrelevance0 ; [ | unshelve eapply eq].
+    9: now eapply over_tree_fusion_l.
+    2: now eapply over_tree_fusion_r.
+    1: now f_equal.
+    1,2: irrelevance0 ; [ | eassumption] ; now f_equal.
+Defined.
+
+Lemma ΣTm_Ltrans (l : TypeLevel) (wl wl' : wfLCon) (Γ : context) (f : wl' ≤ε wl) (A : term)
+  (ΣA : [Γ ||-Σ< l > A ]< wl >)
+  (ΣA' : [Γ ||-Σ< l > A ]< wl' >)
+  (ihdom : forall (Δ : context) (ρ : Δ ≤ Γ) (h : [ |-[ ta ] Δ ]< wl' >) (t : term)
+                  (wl'' : wfLCon) (f' : wl'' ≤ε wl'),
+      [PolyRed.shpRed ΣA ρ f h | Δ ||- t : (ParamRedTy.dom ΣA)⟨ρ⟩ ]< wl' > ->
+      [Ltrans f' (PolyRed.shpRed ΣA ρ f h) | Δ ||- t : (ParamRedTy.dom ΣA)⟨ρ⟩ ]< wl'' >)
+  (ihcod : forall (Δ : context) (a : term) (ρ : Δ ≤ Γ) (h : [ |-[ ta ] Δ ]< wl' >)
+                  (ha : [PolyRed.shpRed ΣA ρ f h | Δ ||- a : (ParamRedTy.dom ΣA)⟨ρ⟩ ]< wl' >)
+                  (wl'' : wfLCon) (Ho : over_tree wl' wl'' (PolyRed.posTree ΣA ρ f h ha))
+                  (t : term) (wl''' : wfLCon) (f'' : wl''' ≤ε wl''),
+      [PolyRed.posRed ΣA ρ f h ha Ho | Δ  ||- t : (ParamRedTy.cod ΣA)[a .: ρ >> tRel] ]< wl'' > ->
+      [Ltrans f'' (PolyRed.posRed ΣA ρ f h ha Ho) | Δ  ||- t : (ParamRedTy.cod ΣA)[a .: ρ >> tRel] ]< wl''' >) :
+  forall (t : term),
+    [Γ ||-Σ t : A | ΣA ]< wl > ->  [Γ ||-Σ t : A | ΣA' ]< wl' >.
+Proof.
+  intros t [].
+  unshelve econstructor.
+  4: eapply redtmwf_Ltrans ; eauto.
+  1: exact nf.
+  2:{ cbn in * ; intros.
+      eapply DTree_fusion.
+      * unshelve eapply sndTree.
+        3: eapply wfLCon_le_trans.
+        2-5: eassumption.
+      * eapply (PolyRed.posTree ΣA ρ (f0 •ε f) Hd).
+        eapply fstRed.
+  }
+  all: unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΣA.(ParamRedTyPack.red)) ΣA'.(ParamRedTyPack.red)) ; [now econstructor | now econstructor | ].
+  all: inversion Heq.
+  3: eapply convtm_Ltrans ; [eauto | ].
+  2,3: cbv ; cbv in Heq ; now rewrite <- Heq.
+  2: eapply isLRPair_Ltrans ; now eauto.
+  + cbn in * ; intros.
+    irrelevance0 ; [ | unshelve eapply fstRed].
+    * now f_equal.
+    * now eapply wfLCon_le_trans.
+    * assumption.
+  + cbn in * ; intros.
+    irrelevance0 ; [ | unshelve eapply sndRed].
+    4: eassumption.
+    * now f_equal.
+    * now eapply wfLCon_le_trans.
+    * now eapply over_tree_fusion_r.
+    * now eapply over_tree_fusion_l.
+Defined.
+  
+Lemma Tm_Ltrans@{h i j k l} {wl Γ wl' t A l} (f : wl' ≤ε wl) (lrA : [Γ ||-<l> A]< wl >) : 
+    [LogRel@{i j k l} l | Γ ||- t : A | lrA]< wl > ->
+    [LogRel@{i j k l} l | Γ ||- t : A | Ltrans@{h i j k l} f lrA]< wl' >.
+Proof.
+  revert t wl' f. pattern l, wl, Γ, A, lrA.
+  eapply LR_rect_TyUr@{i j k l l}; clear l wl Γ A lrA.
+  - intros ???? [??? []] ???[?[]].
+    econstructor ; [ econstructor | eassumption |.. ].
+    + now eapply ty_Ltrans.
+    + now eapply redtm_Ltrans.
+    + now eapply convtm_Ltrans.
+    + apply RedTyRecBwd ; apply RedTyRecFwd in rel.
+      now eapply Ltrans ; eauto.
+  - intros ???? [?[]] ???[?[]] ; cbn in *.
+    econstructor ; [econstructor ; cbn | ].
+    + now eapply ty_Ltrans.
+    + now eapply redtm_Ltrans.
+    + now eapply convneu_Ltrans.
+  - intros ???? [] ihdom ihcod t wl' f ?.
+    cbn in *.
+    unshelve eapply ΠTm_Ltrans ; intros.
+    6: eassumption.
+    1: eassumption.
+    + now eapply ihdom.
+    + now eapply ihcod. 
+  - intros ; irrelevance0 ; [ reflexivity | unshelve eapply NatTm_Ltrans].
+    5: eassumption.
+    2: assumption.
+    destruct NA ; econstructor ; now eapply redtywf_Ltrans.
+  - intros ???? NA t ? f ; revert t ; cbn.
+    intros t Ht. induction Ht. econstructor.
+    + now eapply redtmwf_Ltrans.
+    + now eapply convtm_Ltrans.
+    + destruct prop as [ | | m Hne] ; econstructor.
+      destruct Hne ; econstructor.
+      * now eapply ty_Ltrans.
+      * now eapply convneu_Ltrans.
+  - intros ???? NA t ? f Ht ; cbn.
+    induction Ht ; econstructor.
+    + now eapply redtmwf_Ltrans.
+    + now eapply convtm_Ltrans.
+    + destruct prop as [m Hne] ; econstructor.
+      destruct Hne ; econstructor.
+      * now eapply ty_Ltrans.
+      * now eapply convneu_Ltrans.
+  - intros ????? ihdom ihcod t wl' f ?; cbn in *.
+    eapply ΣTm_Ltrans.
+    + intros ; eauto.
+    + intros ; eauto.
+    + assumption.
+      Unshelve. assumption.
+  - intros * ih1 ih2 *.
+    unshelve eapply IdTm_Ltrans.
+    eassumption.
+    + intros ; eapply ih1 ; auto.
+    + intros ; eapply ih2.
+      rewrite <- (wk_id_ren_on Δ t0).
+      eapply (IdRedTy.tyKripkeTm IA ρ).
+      * now bsimpl.
+      * eassumption.
+Qed.
+
+Lemma WTm_Ltrans@{h i j k l} {wl Γ wl' A t l}
+    (f : wl' ≤ε wl) (lrA : W[Γ ||-<l> A]< wl >) :
+    WLogRelTm@{i j k l} l wl Γ t A lrA ->
+    WLogRelTm@{i j k l} l wl' Γ t A (WLtrans@{h i j k l} f lrA).
+  Proof.
+    intros Ht ; unshelve econstructor.
+    - eapply DTree_Ltrans ; [eassumption | ].
+      exact (WTTm _ Ht).
+    - intros wl'' Hover Hover'.
+      eapply (WRedTm _ Ht).
+      now eapply over_tree_Ltrans.
+  Defined. 
+
+Lemma TmEq_Ltrans@{h i j k l} {wl Γ wl' t u A l} (f : wl' ≤ε wl) (lrA : [Γ ||-<l> A]< wl >) : 
+    [LogRel@{i j k l} l | Γ ||- t ≅ u : A | lrA]< wl > ->
+    [LogRel@{i j k l} l | Γ ||- t ≅ u : A | Ltrans@{h i j k l} f lrA]< wl' >.
+Proof.
+  revert t u wl' f. pattern l, wl, Γ, A, lrA.
+  eapply LR_rect_TyUr@{i j k l l}; clear l wl Γ A lrA.
+  - intros ???? [??? []] ???? [].
+    unshelve econstructor.
+    + destruct redL.
+      econstructor.
+      * now eapply redtmwf_Ltrans.
       * assumption.
+      * now eapply convtm_Ltrans.
+      * apply RedTyRecBwd ; clear relEq ; apply RedTyRecFwd in relL.
+        now eapply Ltrans.
+    + destruct redR.
+      econstructor.
+      * now eapply redtmwf_Ltrans.
       * assumption.
-    + destruct red.
-      split.
-      2: unshelve eapply redty_Ltrans ; try assumption.
-      now eapply wft_Ltrans.
-    + now eapply wft_Ltrans.
-    + now eapply wft_Ltrans.
-    + now eapply convty_Ltrans.
-    + intros ; now eapply codExt.
+      * now eapply convtm_Ltrans.
+      * apply RedTyRecBwd ; clear relEq ; apply RedTyRecFwd in relR.
+        now eapply Ltrans.
+    + apply RedTyRecBwd ; clear relEq ; apply RedTyRecFwd in relL.
+      now eapply Ltrans.
     + cbn in *.
-      econstructor.
-      * intros. now eapply domAd.
-      * intros. now eapply codAd.
-  - unshelve eapply LRNat_.
+      now eapply convtm_Ltrans.
+    + apply RedTyRecBwd ; clear relEq ; apply RedTyRecFwd in relR.
+      now eapply Ltrans.
+    + eapply TyEqRecBwd, Eq_Ltrans ; cbn.
+      now eapply TyEqRecFwd.
+  - intros ???? [?[]] ???? [] ; cbn in *.
     econstructor.
-    destruct red.
-    split ; try now eapply redty_Ltrans.
-    now eapply wft_Ltrans.
-  - unshelve eapply LRBool_.
-    destruct red.
-    econstructor.
-    split ; try now eapply redty_Ltrans.
-    now eapply wft_Ltrans.
-  - unshelve eapply LREmpty_.
-    destruct red.
-    econstructor.
-    split ; try now eapply redty_Ltrans.
-    now eapply wft_Ltrans.
+    + now eapply redtmwf_Ltrans.
+    + now eapply redtmwf_Ltrans.
+    + now eapply convneu_Ltrans.
+  - intros ????? ihdom ihcod t u wl' f [].
+    cbn.
+    unshelve econstructor ; cbn in *.
+    + unshelve eapply ΠTm_Ltrans ; [ | eassumption | ..].
+      1,4: eassumption.
+      * intros ; now eapply Tm_Ltrans.
+      * intros ; now eapply Tm_Ltrans.
+    + unshelve eapply ΠTm_Ltrans ; [ | eassumption | ..].
+      1,4: eassumption.
+      * intros ; now eapply Tm_Ltrans.
+      * intros ; now eapply Tm_Ltrans.
+    + intros ; eapply eqTree.
+      eassumption.
+    + intros ; cbn in *.
+      now eapply convtm_Ltrans.
+    + intros ; cbn in *.
+      eapply eqApp.
+      assumption.
+  - intros * ; revert t u.
+    set (NA' := {| NatRedTy.red := redtywf_Ltrans f (NatRedTy.red NA) |}).
+    set (G := _); enough (h : G × (forall t u, NatPropEq NA t u -> NatPropEq NA' t u)) by apply h.
+    subst G; apply NatRedEqInduction.
+    + intros t u nt nu Hredt Hredu Heq Hprop Hprop'.
+      econstructor.
+      1,2: now eapply redtmwf_Ltrans.
+      * now eapply convtm_Ltrans.
+      * assumption.
+    + now econstructor.
+    + intros n Hn Hn' ; now econstructor.
+    + intros ; econstructor.
+      destruct r ; econstructor.
+      now eapply convneu_Ltrans.
+  - intros ???? NA t ? wl' f Heq.
+    induction Heq ; cbn. econstructor.
+    1,2: now eapply redtmwf_Ltrans.
+    + now eapply convtm_Ltrans.
+    + destruct prop as [ | | m Hne] ; econstructor.
+      econstructor.
+      now destruct r ; eapply convneu_Ltrans.
+  - intros ???? NA t u wl' f Heq ; cbn.
+    induction Heq ; econstructor.
+    1,2: now eapply redtmwf_Ltrans.
+    + now eapply convtm_Ltrans.
+    + destruct prop as [m Hne] ; econstructor ; econstructor.
+      now destruct r ; eapply convneu_Ltrans.
+  - cbn ; intros ????? ihdom ihcod t u wl' f []; cbn in *.
+    unshelve econstructor ; cbn.
+    + unshelve eapply ΣTm_Ltrans.
+      2,3,6: eassumption.
+      * intros.
+        irrelevance0 ; [ | unshelve eapply Tm_Ltrans].
+        5: eassumption.
+        1,2: now auto.
+      * intros.
+        irrelevance0 ; [ | unshelve eapply Tm_Ltrans].
+        5: eassumption.
+        1,2: now trivial.
+    + unshelve eapply ΣTm_Ltrans.
+      2,3,6: eassumption.
+      * intros.
+        irrelevance0 ; [ | unshelve eapply Tm_Ltrans].
+        5: eassumption.
+        1,2: now auto.
+      * intros.
+        irrelevance0 ; [ | unshelve eapply Tm_Ltrans].
+        5: eassumption.
+        1,2: now trivial.
+    + intros ; eapply DTree_fusion.
+      * eapply eqTree.
+        1,3: eassumption.
+        now eapply wfLCon_le_trans.
+      * eapply (PolyRed.posTree ΠA ρ (f0 •ε f) Hd).
+        now eapply (SigRedTm.fstRed redL). 
+    + cbn ; now eapply convtm_Ltrans.
+    + cbn ; intros ; now unshelve eapply eqFst.
+    + cbn in * ; intros.
+      irrelevance0 ; [ reflexivity | unshelve eapply eqSnd].
+      3: eassumption.
+      * now eapply wfLCon_le_trans.
+      * now eapply over_tree_fusion_r.
+      * now eapply over_tree_fusion_l.
+  - intros ????? ih1 ih2 ???? [].
+    unshelve econstructor ; cbn.
+    3,4: now eapply redtmwf_Ltrans.
+    1: now eapply convtm_Ltrans.
+    destruct prop.
+    + econstructor.
+      1,2: now eapply wft_Ltrans.
+      1,2: now eapply ty_Ltrans.
+      1,2:irrelevance0 ; [ | now eapply Eq_Ltrans] ; reflexivity.
+      all: now eapply ih1.
+    + econstructor.
+      destruct r ; econstructor.
+      now eapply convneu_Ltrans.
+      Unshelve. all: assumption.
 Qed.
 
-Lemma LRTyEq_Ltrans@{i j k l i' j' k' l'} lA lA'
-  (wl wl' : wfLCon) (f : wl' ≤ε wl) Γ A        
-  (lrA : [LogRel@{i j k l} lA | Γ ||- A]< wl >)
-  (lrA' : [LogRel@{i' j' k' l'} lA' | Γ ||- A]< wl' >) :
-  forall B, [Γ ||-< lA > A ≅ B | lrA]< wl > ->
-            [Γ ||-< lA' > A ≅ B | lrA']< wl' >.
-Admitted.
-
-
-Lemma LRTm_Ltrans@{i j k l i' j' k' l'} lA lA'
-  (wl wl' : wfLCon) (f : wl' ≤ε wl) Γ A        
-  (lrA : [LogRel@{i j k l} lA | Γ ||- A]< wl >)
-  (lrA' : [LogRel@{i' j' k' l'} lA' | Γ ||- A]< wl' >) :
-  forall t, [Γ ||-< lA > t : A | lrA]< wl > ->
-            [Γ ||-< lA' > t : A | lrA']< wl' >.
-Admitted.
-
-
-Lemma LRTm_Ltrans'@{i j k l i' j' k' l'} lA lA'
-  (wl wl' : wfLCon) (f : wl' ≤ε wl) Γ A        
-  (lrA : [LogRel@{i j k l} lA | Γ ||- A]< wl >)
-  (lrA' : [LogRel@{i' j' k' l'} lA' | Γ ||- A]< wl' >) :
-  forall t, [Γ ||-< lA > t : A | lrA]< wl > ->
-            [Γ ||-< lA' > t : A | lrA']< wl' >.
-Admitted.
-
-
-Lemma LRTmEq_Ltrans@{i j k l i' j' k' l'} lA lA'
-  (wl wl' : wfLCon) (f : wl' ≤ε wl) Γ A        
-  (lrA : [LogRel@{i j k l} lA | Γ ||- A]< wl >)
-  (lrA' : [LogRel@{i' j' k' l'} lA' | Γ ||- A]< wl' >) :
-  forall t u, [Γ ||-< lA > t ≅ u : A | lrA]< wl > ->
-            [Γ ||-< lA' > t ≅ u : A | lrA']< wl' >.
-Admitted.
-(*  intros B eqB.
-  destruct lrA as [ [] lrA] ; cbn in *.
-  induction lrA.
-  
-  cbn.
-  induction lrA as [? ? ? ? | ? | ? ? A [] [] IHdom IHcod|?? NEA|?? NEA |?? NEA].
-  - cbn.
-    unshelve eapply LRTyEqIrrelevantCum ; [exact lA |..].
-    + eapply LRTy_Ltrans ; try eassumption.
-      eapply LRU_ ; econstructor ; eassumption.
-    + cbn.
-  pattern lA, wl, Γ, A, lrA. apply LR_rect_TyUr. clear lA Γ A lrA.
-*)
-
-End Monotonicity.
+Lemma WTmEq_Ltrans@{h i j k l} {wl Γ wl' t u A l}
+    (f : wl' ≤ε wl) (lrA : W[Γ ||-<l> A]< wl >) :
+    WLogRelTmEq@{i j k l} l wl Γ t u A lrA ->
+    WLogRelTmEq@{i j k l} l wl' Γ t u A (WLtrans@{h i j k l} f lrA).
+  Proof.
+    intros Htu ; unshelve econstructor.
+    - eapply DTree_Ltrans ; [eassumption | ].
+      exact (WTTmEq _ Htu).
+    - intros wl'' Hover Hover'.
+      eapply (WRedTmEq _ Htu).
+      now eapply over_tree_Ltrans.
+  Defined. 
+
+End Red_Ltrans.
diff --git a/theories/LogicalRelation/Neutral.v b/theories/LogicalRelation/Neutral.v
index 5371791..b052c2b 100644
--- a/theories/LogicalRelation/Neutral.v
+++ b/theories/LogicalRelation/Neutral.v
@@ -1,7 +1,7 @@
 Require Import PeanoNat.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
 From LogRel Require Import Utils BasicAst Notations LContexts Context NormalForms UntypedReduction Weakening GenericTyping Monad LogicalRelation DeclarativeInstance.
-From LogRel.LogicalRelation Require Import Induction Reflexivity Irrelevance Escape.
+From LogRel.LogicalRelation Require Import Induction Reflexivity Irrelevance Escape Weakening Monotonicity.
 
 Set Universe Polymorphism.
 
@@ -208,17 +208,24 @@ intros l wl Γ A ΠA0 ihdom ihcod; split.
     - now eapply ty_conv.
     - econstructor.
       now eapply convneu_conv.
-    - eapply convneu_app_ren in H20 ; tea ; cycle -1.
-      2: eapply ihcod in H20 as [_ hred].
-      + now eapply escapeEqTerm, reflLRTmEq.
+    - unshelve eapply convtm_over_tree.
+      { now eapply (PolyRed.posTree polyRed _ _ _ X). }
+      intros wl' Hover.
+      pose proof (over_tree_le Hover).
+      eapply (convneu_Ltrans (over_tree_le Hover)) in H20.
+      eapply convneu_app_ren in H20 ; tea ; cycle -1.
+      2: unshelve eapply ihcod in H20 as [_ hred].
+      6: exact Hover.
+      1: now eapply convtm_Ltrans, escapeEqTerm, reflLRTmEq.
+      4: now eapply convty_Ltrans.
       + erewrite <- wk1_ren_on.
         eapply convtm_meta_conv.
         1: now escape.
         1: bsimpl; rewrite scons_eta' ; now bsimpl.
         now bsimpl.
-      + eapply typing_meta_conv ; eauto.
-        bsimpl. rewrite scons_eta'. now bsimpl.
-      + eapply typing_meta_conv ; eauto.
+        + eapply ty_Ltrans, typing_meta_conv ; eauto.
+          bsimpl. rewrite scons_eta'. now bsimpl.
+      + eapply ty_Ltrans, typing_meta_conv ; eauto.
         bsimpl. rewrite scons_eta'. now bsimpl.
   }
 
@@ -243,30 +250,45 @@ intros l wl Γ A ΠA0 ihdom ihcod; split.
           2: eapply convty_Ltrans ; [ | eauto].
           1,2: eapply wfLCon_le_trans ; eassumption.
           all: cbn ; easy.
-        * eapply escapeEqTerm, reflLRTmEq.
+        * unshelve eapply escapeEqTerm, reflLRTmEq, Tm_Ltrans.
+          3,5: eassumption.
         * now bsimpl.
-        * reflexivity. 
-      + eapply Happ ; tea.
-        now escape.
+        * reflexivity.
+      + eapply Happ.
+        * now eapply wfLCon_le_trans.
+        * now eapply wfc_Ltrans.
+        * now eapply ty_Ltrans ; [now eapply wfLCon_le_trans | ].
+        * now eapply ty_Ltrans ; [ | now escape].
       + eapply Happ ; tea.
-        now escape.
+        * now eapply wfLCon_le_trans.
+        * now eapply wfc_Ltrans.
+        * now eapply ty_Ltrans ; [now eapply wfLCon_le_trans | ].
+        * now eapply ty_Ltrans ; [ | now escape].
     - intros.
       eapply ihcod ; last first.
-      + eapply convne_meta_conv.
+      + eapply convneu_Ltrans ; [eassumption | ].
+        eapply convne_meta_conv.
         1: eapply convneu_app.
         * eapply convne_meta_conv.
           1: eapply convneu_wk.
-          2: eapply convneu_conv ; tea.
+          2: eapply convneu_Ltrans, convneu_conv ; [eassumption | ..] ; tea.
           all: cbn ; easy.
         * now escape.
         * now bsimpl.
         * reflexivity. 
-      + eapply ty_conv.
-        1: eapply Happ ; tea ; now escape.
-        symmetry.
-        eapply escapeEq, PolyRed.posExt ; tea.
-      + eapply Happ ; tea.
-        now escape.
+      + unshelve eapply ty_conv.
+        2: eapply Happ ; tea.
+        5:{ symmetry.
+            unshelve eapply escapeEq, PolyRed.posExt.
+            8: eassumption. all: eassumption.
+        }
+        * now eapply wfLCon_le_trans.
+        * now eapply wfc_Ltrans.
+        * now eapply ty_Ltrans ; [ eapply wfLCon_le_trans | ].
+        * now eapply ty_Ltrans ; [ eassumption | escape ].
+      + eapply ty_Ltrans, Happ ; [now eauto | ..] ; tea.
+        2:now escape.
+        now eapply ty_Ltrans.
   }
 
   intros ???? h.
@@ -275,385 +297,287 @@ intros l wl Γ A ΠA0 ihdom ihcod; split.
   unshelve econstructor.
   1,2: now apply funred.
   all: cbn; clear funred.
-  * eauto.
-  * intros. apply ihcod; cbn.
-    + apply escapeTerm in ha; now eapply ty_app_ren.
-    + apply escapeTerm in ha; now eapply ty_app_ren.
-    + eapply convneu_app_ren. 1,2: eassumption.
-    eapply escapeEqTerm; eapply reflLRTmEq; eassumption.
-
-  Unshelve.
-  all: eauto.
+  2: now eauto.
+  + intros.
+    now eapply leaf.
+  + intros. apply ihcod; cbn.
+    1,2: eapply ty_Ltrans ; [now eapply over_tree_le | ].
+    1,2: pose proof (escapeTerm _ ha); eapply ty_app_ren.
+    all: try eassumption.
+    1,3: now eapply ty_Ltrans.
+    1,2: now eapply convty_Ltrans.
+    eapply convneu_Ltrans, convneu_app_ren ; [now eapply over_tree_le |.. ].
+    3: eapply escapeEqTerm; eapply reflLRTmEq ; eassumption.
+    1: now eapply convneu_Ltrans.
+    now eapply convty_Ltrans.
 Qed.
 
 Arguments ParamRedTy.outTy /.
 
-Record complete {l wl Γ A} (RA : [Γ ||-<l> A]< wl >) := {
-  reifyTyConvN :
-    forall B,
-      [Γ ||-<l> A ≅ B | RA]< wl > -> nat ;
-  reifyTyConv :
-    forall B (convB : [Γ ||-<l> A ≅ B | RA]< wl >)
-           (wl' : wfLCon) (τ : wl' ≤ε wl)
-           (Ninfl : reifyTyConvN B convB  <= length wl'),
-        Nf[Γ |- B]< wl' > ;
-  reflect : forall n n',
-    Ne[Γ |- n : A]< wl > ->
-    Ne[Γ |- n' : A]< wl > ->
-    [Γ |- n : A]< wl > ->
-    [Γ |- n' : A]< wl > ->
-    [Γ |- n ~ n' : A]< wl > ->
-    [Γ ||-<l> n : A | RA]< wl > × [Γ ||-<l> n ≅ n' : A| RA]< wl > ;
-  reifyN : forall a, [Γ ||-<l> a : A | RA]< wl > -> nat ;
-  reify : forall a (ha : [Γ ||-<l> a : A | RA]< wl >)
-                 (wl' : wfLCon) (τ : wl' ≤ε wl)
-                 (Ninfl : reifyN a ha  <= length wl'),
-                   Nf[ Γ |- a : A]< wl' > ;
-  }.
-
-(*Record complete  {l wl Γ A} (RA : [Γ ||-<l> A]< wl >) := {
-  reifyTyConv :
-    forall B (convB : [Γ ||-<l> A ≅ B | RA]< wl >),
-        Nf[Γ |- B]< wl > ;
-  reflect : forall n n',
-    Ne[Γ |- n : A]< wl > ->
-    Ne[Γ |- n' : A]< wl > ->
-    [Γ |- n : A]< wl > ->
-    [Γ |- n' : A]< wl > ->
-    [Γ |- n ~ n' : A]< wl > ->
-    [Γ ||-<l> n : A | RA]< wl > × [Γ ||-<l> n ≅ n' : A| RA]< wl > ;
-  reify : forall a (ha : [Γ ||-<l> a : A | RA]< wl >),
-      Nf[ Γ |- a : A]< wl > ;
-    }.*)
 
-Lemma complete_reflect_simpl {l wl Γ A} (RA : [Γ ||-<l> A]< wl >) (c : complete RA) :
-  forall n, Ne[Γ |- n : A]< wl > -> [Γ |- n : A]< wl > -> [Γ |- n ~ n : A]< wl > -> [Γ ||-<l> n : A | RA]< wl >.
-Proof.
-intros; eapply c.
-5: eassumption.
-all: assumption.
-Qed.
-
-Lemma complete_var0 {l wl Γ A A'} (RA : [Γ ,, A ||-<l> A']< wl >) :
-  complete RA ->
-  [Γ ,, A |- A⟨↑⟩ ≅ A']< wl > ->
-  [Γ |- A]< wl > ->
-  [Γ ,, A ||-<l> tRel 0 : A' | RA]< wl >.
-Proof.
-  intros cRA conv HA.
-  assert [Γ ,, A |- tRel 0 : A']< wl >
-  by (eapply ty_conv; tea; escape; eapply (ty_var (wfc_wft EscRA) (in_here _ _))).
-  eapply complete_reflect_simpl; tea.
-  - eapply tm_ne_conv; tea. 
-    now eapply tm_ne_rel.
-  - eapply convneu_var; tea.
-Qed.
 
-
-Lemma complete_U : forall l wl Γ A (RA : [Γ ||-U< l > A]< wl >),
-    complete (LRU_ RA).
-Proof.
-  intros l wl Γ A h0.
-  unshelve econstructor.
-  - exact (fun _ _ => 0).
-  - exact (fun _ _ => 0).
-  - intros ? [] ???.
-    eapply ty_nf_red, ty_nf_sort ; gen_typing.
-  - intros ?? ???? h; pose proof (lrefl h); pose proof (urefl h).
-    assert [Γ |- A ≅ U]< wl > by (destruct h0; gen_typing); split.
-    2: unshelve econstructor.
-    1-3: now apply neU.
-    + eapply RedTyRecBwd, neu. 2,3: try gen_typing.
-      eapply ty_ne_term, tm_ne_conv; tea; gen_typing.
-    + cbn. gen_typing.
-    + eapply RedTyRecBwd; apply neu. 2, 3: gen_typing.
-      eapply ty_ne_term, tm_ne_conv; tea; gen_typing.
-    + eapply TyEqRecBwd. eapply neuEq. all: try gen_typing.
-      all: eapply ty_ne_term, tm_ne_conv; tea; gen_typing.
-  - intros a [a' Hr Ha] ???.
-    assert ([Γ |-[ ta ] U ≅ A]< wl >).
-    { destruct h0; gen_typing. }
-    eapply tm_nf_conv ; try easy.
-    + eapply tm_nf_red; [eapply tmr_wf_red|].
-      gen_typing.
-      eapply tm_nf_red.
-      now gen_typing.
-      eapply tm_nf_Ltrans ; [ | eassumption].
-      assumption.
-    + eapply convty_Ltrans ; [ | eassumption].
-      assumption.
-Qed.
-
-Lemma complete_ne : forall l wl Γ A (RA : [Γ ||-ne A]< wl >),
-    complete (LRne_ l RA).
+Lemma complete_Sig : forall l wl Γ A (RA : [Γ ||-Σ< l > A]< wl >),
+  (forall (Δ : context) (wl' : wfLCon) (ρ : Δ ≤ Γ) (f : wl' ≤ε wl) (h : [ |-[ ta ] Δ]< wl' >),
+        complete (PolyRed.shpRed RA ρ f h)) ->
+  (forall (Δ : context) (wl' : wfLCon) (a : term) (ρ : Δ ≤ Γ) (f : wl' ≤ε wl) (h : [ |-[ ta ] Δ]< wl' >)
+          (ha : [PolyRed.shpRed RA ρ f h | Δ ||- a : _]< wl' >)
+          (wl'' : wfLCon) (Ho : over_tree wl' wl'' (PolyRed.posTree RA ρ f h ha)),
+        complete (PolyRed.posRed RA ρ f h ha Ho)) ->
+  complete (LRSig' RA).
 Proof.
-  intros l wl Γ A h0. unshelve econstructor.
-  - exact (fun _ _ => 0).
-  - exact (fun _ _ => 0).
-  - intros ? [] ???.
-    eapply ty_nf_red.
-    eapply redty_Ltrans ; try now destruct red.
-    now eapply ty_nf_Ltrans ; try now apply ty_ne_nf.
-  - destruct h0 as [B []]; intros ** ; assert ([Γ |- A ≅ B]< wl >) by gen_typing ;
-      split.
-  + exists n; cbn.
-    * eapply redtmwf_refl ; gen_typing.
-    * now eapply tm_ne_conv.
-    * eapply lrefl; eapply convneu_conv; eassumption.
-  + exists n n'; cbn.
-    1,2: eapply redtmwf_refl ; eapply ty_conv; gen_typing.
-    1,2: now eapply tm_ne_conv.
-    gen_typing.
-- intros a [a' Hr Hne] ???.
-  assert ([Γ |-[ ta ] neRedTy.ty h0 ≅ A]< wl >).
-  { destruct h0; simpl in *; symmetry.
-    eapply convty_exp; [now apply tyr_wf_red| |].
-    all: gen_typing. }
-  eapply tm_nf_Ltrans.
-  eassumption.
-  eapply tm_nf_conv; [|eassumption].
-  + eapply tm_nf_red; [now apply tmr_wf_red|].
-    now apply tm_ne_nf.
-Qed.
+  intros l wl Γ A ΣA0 ihdom ihcod.
+  set (ΣA := ΣA0); destruct ΣA0 as [dom cod] ; cbn in *.
 
-(*Lemma complete_Pi : forall l wl Γ A (RA : [Γ ||-Π< l > A]< wl >),
-  (forall (Δ : context) (wl' : wfLCon) (ρ : Δ ≤ Γ) (τ : wl' ≤ε wl)
-          (Ninfl : (PiRedTyPack.domN RA) <= length wl')
-          (h : [ |-[ ta ] Δ]< wl' >),
-        complete (PiRedTyPack.domRed RA ρ τ Ninfl h)) ->
-  (forall (Δ : context) (a : term) (wl' : wfLCon)
-          (ρ : Δ ≤ Γ) (τ : wl' ≤ε wl)
-          (Ninfl : (PiRedTyPack.domN RA) <= length wl')
-          (h : [ |-[ ta ] Δ]< wl' >)
-          (ha : [PiRedTyPack.domRed RA ρ τ Ninfl h | Δ ||- a : (PiRedTyPack.dom RA)⟨ρ⟩]< wl' >)
-          {wl'' : wfLCon}
-          (τ' : wl'' ≤ε wl')
-          (Minfl : PiRedTyPack.codomN RA ρ τ Ninfl h ha <= length wl''),
-        complete (PiRedTyPack.codRed RA ρ τ Ninfl h ha τ' Minfl)) ->
-  complete (LRPi' RA).
-Proof.
-  intros l wl Γ A ΠA0 ihdom ihcod.
-  unshelve esplit.
-  - intros B ΠB.
-    exact (max (PiRedTyPack.domN ΠA0) (PiRedTyEq.domN ΠB)).
-  - admit.
-  - intros B ΠB ???.
-    assert (tΓ : [|- Γ]< wl >) by (destruct ΠA0; gen_typing).
-(*      eapply ty_nf_red ; try now apply tyr_wf_red, ΠB.
-    
-    eapply ty_nf_prod.
-    * Search le minus 0.
-      remember (max (PiRedTyPack.domN ΠA0) (PiRedTyEq.domN ΠB) - length wl) as m.
-      revert wl tΓ ΠA0 ΠB ihdom ihcod Heqm.
-      induction m ; intros.
-      unshelve eapply ihdom.
-      -- exact wk_id.
-      -- now eapply wfLCon_le_id.
-      -- eapply Nat.max_lub_l.
-         eapply Nat.sub_0_le.
-         now erewrite <- Heqm.
-      -- assumption.
-      -- erewrite <- wk_id_ren_on; eapply (PiRedTyEq.domRed ΠB).
-         eapply Nat.max_lub_r.
-         eapply Nat.sub_0_le.
-         now erewrite <- Heqm.
-      -- assert (ty_nf_ϝ : forall A n (ne : not_in_LCon (pi1 wl) n), 
-                    Nf[ Γ |- A ]< wl ,,l (ne, true) > ->
-                    Nf[ Γ |- A ]< wl ,,l (ne, false) > ->
-                    Nf[ Γ |- A ]< wl > ).
-         admit.
-         assert (not_in_LCon wl 0) as Hyp.
-         admit.
-         unshelve eapply ty_nf_ϝ.
-         ++ exact 0.
-         ++ assumption.
-         ++ pose (test := IHm (wl,,l (Hyp, true))
-                            (wfc_Ltrans (LCon_le_step _ (wfLCon_le_id _)) tΓ)).
-            eapply test.
-         eapply Nat.sub_0_le.
-         generalize (PiRedTyEq.domN ΠB).
-         clear ihdom ihcod ΠA0 ΠB A B tΓ.
-         intro n.
-         remember (n - #|wl|) as m.
-         revert wl Heqm.
-         induction m.
-         
-         ++ reflexivity.
-         ++ intros.
-         (* Faire autant de splits que néccessaire pour que domN A et domN B
-            soient < length wl *)
-         eapply ty_nf_prod.
-
-  
-    unshelve refine (max (max (PiRedTyPack.domN ΠA0) (PiRedTyEq.domN ΠB)) _).
-    unshelve eapply ihdom.
-  - intros B ΠB.
-    exact (PiRedTyPack.domN ΠA0).
-  - cbn ; intros B ΠB * f Ninfl.
-    assert (tΓ : [|- Γ]< wl >) by (destruct ΠA0; gen_typing).*)
-    eapply ty_nf_red.
-    + eapply redty_Ltrans ; try easy.
-      apply tyr_wf_red, ΠB.
-    + eapply ty_nf_prod.
-      * destruct (ihdom Γ wl' (wk_id) τ (Nat.max_lub_l _ _ _ Ninfl) (wfc_Ltrans τ tΓ)).
-        cbn in *.
-        unshelve eapply ihdom.
-        -- exact wl'.
-        -- exact wk_id.
-        -- assumption.
-        -- now eapply Nat.max_lub_l.
-        -- now eapply wfc_Ltrans.
-        -- erewrite <- wk_id_ren_on.
-           eapply (PiRedTyEq.domRed ΠB) ; now eapply Nat.max_lub_r.
-        -- now eapply wfLCon_le_id.
-        -- cbn.
-            assert (forall (wl' : wfLCon) (τ : wl' ≤ε wl)
-                 (Ninfl : (PiRedTyPack.domN ΠA0) <= length wl'),
-                 [PiRedTyPack.domRed ΠA0 wk_id τ Ninfl (wfc_Ltrans τ tΓ) | Γ ||- (PiRedTyPack.dom ΠA0)⟨wk_id⟩ ≅ PiRedTyEq.dom ΠB]< wl >).
-  1: erewrite <- wk_id_ren_on; eapply (PiRedTyEq.domRed ΠB).
-  eapply ty_nf_prod.
-  + now eapply ihdom.
-  + unshelve eapply ihdom.
-    * exact wk_id.
-    * now eapply wfLCon_le_id.
-    * 
-  assert [forall (wl' : wfLCon) (τ : wl' ≤ε wl)
-                 (Ninfl : (PiRedTyPack.domN RA) <= length wl'),
-        PiRedTyPack.domRed ΠA0 wk_id tΓ | Γ ||- (PiRedTyPack.dom ΠA0)⟨wk_id⟩ ≅ PiRedTyEq.dom ΠB]< wl >.
-  1: erewrite <- wk_id_ren_on; eapply (PiRedTyEq.domRed ΠB).
-  eapply ty_nf_prod.
-  + now eapply ihdom.
-  + destruct ΠB as [dom cod ?? domRed codRed] ; cbn in *.
-    assert [|- Γ ,, dom]. 1:{
-      apply wfc_cons; tea.
-      now eapply escapeConv.
-    }
-    eapply ihcod.
+  assert [Γ |- A ≅ ΣA.(outTy)]< wl >
+    by (destruct ΣA; cbn in *; gen_typing).
+  assert [Γ |- ΣA.(outTy)]< wl >
+    by (destruct ΣA; cbn in *; gen_typing).
+  assert [Γ |- dom]< wl >.
+  {
+    erewrite <- wk_id_ren_on.
+    eapply escape, polyRed.
+    + now eapply wfLCon_le_id.
+    + now gen_typing.
+  } 
+  assert [|- Γ ,, dom]< wl > as Hext by gen_typing.
+  assert [Γ,, dom |-[ ta ] tRel 0 : dom⟨@wk1 Γ dom⟩]< wl >.
+  {
+    eapply ty_var ; tea.
+    rewrite wk1_ren_on.
+    now econstructor.
+  }
+  assert [Γ,, dom |-[ ta ] tRel 0 ~ tRel 0 : dom⟨@wk1 Γ dom⟩]< wl >
+    by now apply convneu_var.
+  assert [PolyRed.shpRed polyRed (wk1 dom) (wfLCon_le_id _) Hext | Γ,, dom ||- tRel 0 : dom⟨wk1 dom⟩]< wl >
+    by now eapply ihdom.
+  assert [Γ ,, dom |- cod]< wl >.
+  {
     replace cod with cod[tRel 0 .: @wk1 Γ dom >> tRel].
-    2: bsimpl ; rewrite scons_eta' ; now bsimpl.
-    eapply codRed.
-    Unshelve.  1: tea.
-    eapply complete_var0.
-      * eapply ihdom.
-      * symmetry; eapply escapeEq; erewrite <- wk1_ren_on.
-        unshelve eapply domRed. tea.
-      * now eapply escapeConv.
-- set (ΠA := ΠA0); destruct ΠA0 as [dom cod].
-  simpl in ihdom, ihcod.
-  assert [Γ |- A ≅ tProd dom cod]< wl > by gen_typing.
-  unshelve refine ( let funred : forall n, Ne[Γ |- n : A]< wl > -> [Γ |- n : A]< wl > -> [Γ |- n ~ n : A]< wl > -> [Γ ||-Π n : A | PiRedTyPack.toPiRedTy ΠA]< wl > := _ in _).
+    2: bsimpl; rewrite scons_eta'; now asimpl.
+    unshelve eapply (wft_over_tree).
+    + exact (PolyRed.posTree polyRed _ _ _ X).
+    + intros wl' Hover.
+      unshelve eapply escape, polyRed.
+      5: eassumption.
+  }
+  assert (hfst : forall n Δ wl' (ρ : Δ ≤ Γ) (f : wl' ≤ε wl) (h : [ |- Δ]< wl' >),
+             [Γ |- n : A]< wl' > -> [Γ |- n ~ n : A]< wl' > ->
+             [PolyRedPack.shpRed ΣA ρ f h | Δ ||- tFst n⟨ρ⟩ : _]< wl' >).
+    1:{
+      intros; eapply complete_reflect_simpl.
+      * now eapply ihdom.
+      * rewrite wk_fst; eapply ty_wk; tea.
+        eapply ty_fst, ty_conv ; [eassumption | ].
+        now eapply convty_Ltrans.
+      * rewrite wk_fst; eapply convneu_wk; tea.
+        eapply convneu_fst, convneu_conv ; [eassumption | ].
+        now eapply convty_Ltrans.
+    }
+    assert (hconv_fst : forall n n' Δ wl' (ρ : Δ ≤ Γ) (f : wl' ≤ε wl) (h : [ |- Δ]< wl' >),
+               [Γ |- n : A]< wl' > -> [Γ |- n' : A]< wl' > -> [Γ |- n ~ n' : A]< wl' > ->
+               [PolyRedPack.shpRed ΣA ρ f h | Δ ||- tFst n⟨ρ⟩ ≅ tFst n'⟨ρ⟩ : _]< wl' >).
+    1:{
+      intros.
+      eapply ihdom.
+      * rewrite wk_fst; eapply ty_wk; tea.
+        eapply ty_fst, ty_conv ; [eassumption | now eapply convty_Ltrans].
+      * rewrite wk_fst ; eapply ty_wk ; tea.
+        eapply ty_fst, ty_conv ; [eassumption | now eapply convty_Ltrans].
+      * repeat rewrite wk_fst; eapply convneu_wk; tea.
+        eapply convneu_fst, convneu_conv ; [eassumption | now eapply convty_Ltrans].
+    }
+  assert (hconv : forall n n',
+  [Γ |- n : A]< wl > -> [Γ |- n' : A]< wl > ->
+  [Γ |- n ~ n : A]< wl > -> [Γ |- n' ~ n' : A]< wl > ->
+  [Γ |- n ~ n' : A]< wl > -> [Γ |-[ ta ] n ≅ n' : tSig dom cod]< wl >).
   {
-    intros. exists n; cbn.
-    * eapply redtmwf_refl ; gen_typing.
-    * now eapply NeFun, tm_ne_whne.
-    * eapply tm_nf_conv; [| |eassumption].
-      + now eapply tm_ne_nf.
-      + now eapply wft_prod.
-    * gen_typing.
-    * intros; apply complete_reflect_simpl; [apply ihcod| |..].
-      { eapply neu_app_ren; try eassumption.
-        + now apply wft_prod.
-        + now apply (ihdom _ ρ h). }
-      1: escape ; now eapply ty_app_ren.
-      eapply convneu_app_ren. 1,2: eassumption.
-      eapply LREqTermRefl_ in ha.
-      now escape.
-    * intros. apply ihcod.
-      + eapply neu_app_ren; try eassumption.
-        -- now apply wft_prod.
-        -- now apply (ihdom _ ρ h).
-      + eapply tm_ne_conv.
-        - eapply neu_app_ren; try eassumption.
-          -- now apply wft_prod.
-          -- now apply (ihdom _ ρ h).
-        - now eapply escape, codRed.
-        - symmetry. now unshelve eapply escapeEq, codExt.
-      + apply escapeTerm in ha; now eapply ty_app_ren.
-      + pose proof (cv := escapeEq _ (codExt _ _ _ ρ _ ha hb eq0)).
-        symmetry in cv; unshelve eapply (ty_conv _ cv).
-        apply escapeTerm in hb; now eapply ty_app_ren.
-      + apply escapeEqTerm in eq0; now eapply convneu_app_ren.
+    intros.
+    eapply convtm_eta_sig ; cbn in * ; tea.
+    - now eapply ty_conv.
+    - econstructor.
+      now eapply convneu_conv.
+    - now eapply ty_conv.
+    - econstructor.
+      now eapply convneu_conv.
+    - eapply convtm_meta_conv.
+      1: eapply escapeEqTerm, ihdom.
+      4: now rewrite wk_id_ren_on.
+      4: reflexivity.
+      all: rewrite wk_id_ren_on.
+      + now eapply ty_fst, ty_conv.
+      + now eapply ty_fst, ty_conv.
+      + eapply convneu_fst, convneu_conv ; tea.
+      Unshelve.
+        * now eapply wfLCon_le_id.
+        * now gen_typing.
+    - eapply convtm_meta_conv.
+      3: reflexivity.
+      1: unshelve eapply convtm_over_tree.
+      2: intros ; eapply escapeEqTerm, (ihcod _ _ (tFst n) wk_id).
+      Unshelve.
+      1: unshelve eapply ((PolyRed.posTree polyRed wk_id (wfLCon_le_id _))).
+      2: now gen_typing.
+      11: exact H21.
+      5: rewrite <- (wk_id_ren_on Γ n) ; now eapply hfst.
+      1,2,3: pose proof (Hyp := over_tree_le H21).
+      + eapply typing_meta_conv.
+        eapply ty_snd, ty_conv ; [now eapply ty_Ltrans | ].
+        now eapply convty_Ltrans.
+        now bsimpl.
+      + eapply ty_conv.
+        eapply ty_snd, ty_conv ; [now eapply ty_Ltrans | ].
+        now eapply convty_Ltrans.
+        symmetry.
+        replace (cod[(tFst n')..]) with (cod[(tFst n') .: (@wk_id Γ) >> tRel]) by (now bsimpl).
+        erewrite <- (wk_id_ren_on _ n), <- (wk_id_ren_on _ n').
+        unshelve eapply escapeEq, polyRed.(PolyRed.posExt).
+        4: now eapply hfst.
+        4: now eapply hfst.
+        now eapply wfLCon_le_id.
+        now gen_typing.
+        2: now eapply hconv_fst.
+        revert H21 ; now destruct (wk_id_ren_on Γ n).
+      + eapply convneu_Ltrans ; [eassumption | ].
+        eapply convne_meta_conv.
+        1:now eapply convneu_snd, convneu_conv.
+        1: now bsimpl.
+        easy.
+      + now bsimpl.
   }
-  intros ?????? h.
-  pose proof (lrefl h); pose proof (urefl h).
-  split. 1: now apply funred.
-  unshelve econstructor.
-  1,2: now apply funred.
-  all: cbn; clear funred.
-  * gen_typing.
-  * intros. apply ihcod; cbn.
-    + eapply neu_app_ren; try eassumption.
-      -- now apply wft_prod.
-      -- now eapply (ihdom _ ρ).
-    + eapply neu_app_ren; try eassumption.
-      -- now apply wft_prod.
-      -- now eapply (ihdom _ ρ).
-    + apply escapeTerm in ha; now eapply ty_app_ren.
-    + apply escapeTerm in ha; now eapply ty_app_ren.
-    + eapply convneu_app_ren. 1,2: eassumption.
-    eapply escapeEqTerm; eapply LREqTermRefl_; eassumption.
-- intros a [a' Hr Ha].
-  destruct ΠA0 as [dom codom]; simpl in *.
-  assert ([Γ |- tProd dom codom ≅ A ]< wl >) by gen_typing.
-  eapply tm_nf_conv; [| |eassumption].
-  * eapply tm_nf_red; [now apply tmr_wf_red|].
-    assumption.
-  * destruct red; gen_typing.
+  split.
+  unshelve refine ( let funred : forall n,
+    [Γ |- n : A]< wl > ->
+    [Γ |- n ~ n : A]< wl > -> [Γ ||-Σ n : A | ΣA]< wl > := _ in _).
+  {
+    intros n **.
+    cbn in *.
+    unshelve eexists n _ _.
+    - intros. eapply hfst.
+      + now eapply ty_Ltrans.
+      + now eapply convneu_Ltrans.
+    - intros ; now eapply leaf. 
+    - eapply redtmwf_refl; now eapply ty_conv.
+    - eauto.
+    - constructor ; cbn ; now eapply convneu_conv.
+    - intros.
+      cbn.
+     pose proof (Hyp := over_tree_le Ho).
+      eapply complete_reflect_simpl.
+      * eapply ihcod.
+      * rewrite wk_snd.
+        eapply typing_meta_conv.
+        1: eapply ty_wk ; tea.
+        1: now eapply wfc_Ltrans.
+        1: eapply ty_snd, ty_conv.
+        1: now eapply ty_Ltrans ; [ eapply wfLCon_le_trans | ].
+        now eapply convty_Ltrans ; [eapply wfLCon_le_trans | ].
+        now bsimpl.
+      * eapply convneu_Ltrans ; [eassumption | ].
+        eapply convne_meta_conv.
+        3: reflexivity.
+        1: rewrite wk_snd.
+        1: eapply convneu_wk ; tea.
+        1: eapply convneu_Ltrans ; [eassumption | ].
+        1: now eapply convneu_snd, convneu_conv.
+        now bsimpl.
+  }
+
+  intros ???? h.
+  pose proof (lrefl h); pose proof (urefl h).  
+  unshelve refine (let Rn :[Γ ||-Σ n : A | ΣA]< wl > := _ in _).
+    1: eapply funred; tea; now eapply lrefl.
+    unshelve refine (let Rn' :[Γ ||-Σ n' : A | ΣA]< wl > := _ in _).
+    1: eapply funred; tea; now eapply urefl.
+    assert (forall Δ wl' (ρ : Δ ≤ Γ) (f : wl' ≤ε wl) (h : [ |- Δ]< wl' >),
+      [Δ |- cod[tFst n⟨ρ⟩ .: ρ >> tRel] ≅ cod[tFst n'⟨ρ⟩ .: ρ >> tRel]]< wl' >).
+    { intros ; eapply convty_over_tree.
+      intros wl'' Ho ; eapply escapeEq; unshelve eapply (PolyRed.posExt ΣA).
+      2,3,5: eassumption.
+      + eapply Rn.
+      + eapply Rn'.
+      + eapply hconv_fst.
+        1,2: now eapply ty_Ltrans.
+        now eapply convneu_Ltrans.
+    }
+    split; tea; unshelve eexists Rn Rn' _.
+    + intros ; now eapply leaf.
+    + cbn.
+      eapply hconv ; tea.
+    + cbn. intros. eapply hconv_fst.
+      1,2: now eapply ty_Ltrans.
+      now eapply convneu_Ltrans.
+    + intros; cbn; eapply ihcod.
+      all: pose proof (Hyp := over_tree_le Ho).
+      1,2: eapply ty_Ltrans ; [eassumption | ].
+      3: eapply convneu_Ltrans ; [eassumption | ].
+      all: rewrite wk_fst; rewrite !wk_snd.
+      2: eapply ty_conv; [| symmetry ; eapply H20 ; eauto].
+      2: rewrite wk_fst.
+      all: rewrite <- subst_ren_subst_mixed.
+      1,2: eapply ty_wk ; tea.
+      1,2: eapply ty_Ltrans ; [eassumption | ].
+      1,2: now eapply ty_snd, ty_conv.
+      * eapply convneu_wk; tea.
+        eapply convneu_snd, convneu_Ltrans ; [eassumption | ].
+        now eapply convneu_conv.
 Qed.
 
+
+
+
 Lemma complete_Nat {l wl Γ A} (NA : [Γ ||-Nat A]< wl >) : complete (LRNat_ l NA).
 Proof.
   split.
-  - intros ? [].
-    eapply ty_nf_red, ty_nf_nat; gen_typing.
   - intros. 
     assert [Γ |- A ≅ tNat]< wl > by (destruct NA; gen_typing). 
     assert [Γ |- n : tNat]< wl > by now eapply ty_conv.
     split; econstructor.
     1,4,5: eapply redtmwf_refl; tea; now eapply ty_conv.
     2,4: do 2 constructor; tea.
-    1,7: eapply convtm_convneu.
-    1,4: eapply lrefl.
-    4-6: now (eapply tm_ne_conv; gen_typing).
-    all: eapply convneu_conv; tea.
-  - simpl in *.
-    assert [Γ |- tNat ≅ A]< wl > by (destruct NA; gen_typing).
-    assert [Γ |- A]< wl > by now (destruct NA; gen_typing).
-    intros a Ha; eapply tm_nf_conv; [|eassumption|eassumption]; revert a Ha.
-    let T := match goal with |- ?P => P end in
-    enough (IH : T × (forall (a : term) (n : NatProp NA a), Nf[ Γ |-[ ta ] a : tNat]< wl >)); [apply IH|].
-    apply NatRedInduction.
-    + intros.
-      eapply tm_nf_red; [now apply tmr_wf_red|eassumption].
-    + eapply tm_nf_zero; gen_typing.
-    + intros; now eapply tm_nf_succ.
-    + intros ne []. apply tm_ne_nf. assumption.
+    1,4: eapply convtm_convneu ; [now constructor|..].
+    all: eapply convneu_conv; [|eassumption].
+    all: first [assumption|now eapply lrefl].
 Qed.
 
 Lemma complete_Empty {l wl Γ A} (NA : [Γ ||-Empty A]< wl >) : complete (LREmpty_ l NA).
 Proof.
   split.
-  - intros ? [].
-    eapply ty_nf_red, ty_nf_empty; gen_typing.
   - intros. 
     assert [Γ |- A ≅ tEmpty]< wl > by (destruct NA; gen_typing). 
     assert [Γ |- n : tEmpty]< wl > by now eapply ty_conv.
     split; econstructor.
     1,4,5: eapply redtmwf_refl; tea; now eapply ty_conv.
     2,4: do 2 constructor; tea.
-    1,7: eapply convtm_convneu.
-    1,4: eapply lrefl.
-    4-6: now (eapply tm_ne_conv; gen_typing).
-    all: eapply convneu_conv; tea.
-  - simpl in *.
-    assert [Γ |- tEmpty ≅ A]< wl > by (destruct NA; gen_typing).
-    intros a Ha; eapply tm_nf_conv; [| |eassumption].
-    + destruct Ha.
-      destruct prop.
-      destruct r.
-      eapply tm_nf_red. exact red.
-      now apply tm_ne_nf.
-    + destruct NA as [[]]; gen_typing.
+    1,4: eapply convtm_convneu ; [now constructor|..].
+    all: eapply convneu_conv; [|eassumption].
+    all: try first [assumption|now eapply lrefl].
+Qed.
+
+Lemma complete_Bool {l wl Γ A} (NA : [Γ ||-Bool A]< wl >) : complete (LRBool_ l NA).
+Proof.
+  split.
+  - intros. 
+    assert [Γ |- A ≅ tBool]< wl > by (destruct NA; gen_typing). 
+    assert [Γ |- n : tBool]< wl > by now eapply ty_conv.
+    split; econstructor.
+    1,4,5: eapply redtmwf_refl; tea; now eapply ty_conv.
+    2,4: do 2 constructor; tea.
+    1,4: eapply convtm_convneu ; [now constructor|..].
+    all: eapply convneu_conv; [|eassumption].
+    all: try first [assumption|now eapply lrefl].
+Qed.
+
+Lemma complete_Id {l wl Γ A} (IA : [Γ ||-Id<l> A]< wl >) :
+  complete (LRId' IA).
+Proof.
+  split; intros.
+  assert [Γ |- A ≅ IA.(IdRedTy.outTy)]< wl > by (destruct IA; unfold IdRedTy.outTy; cbn; gen_typing).
+  assert [Γ |- n : IA.(IdRedTy.outTy)]< wl > by now eapply ty_conv.
+  split; econstructor.
+  1,4,5: eapply redtmwf_refl; tea; now eapply ty_conv.
+  2,4: do 2 constructor; tea.
+  1,4: eapply convtm_convneu ; [now constructor|..].
+  all: eapply convneu_conv; tea; now eapply lrefl.
 Qed.
 
 Lemma completeness {l wl Γ A} (RA : [Γ ||-<l> A]< wl >) : complete RA.
@@ -663,11 +587,13 @@ revert l wl Γ A RA; eapply LR_rect_TyUr; cbn; intros.
 - now apply complete_ne.
 - now apply complete_Pi.
 - now apply complete_Nat.
+- now apply complete_Bool.
 - now apply complete_Empty.
+- now apply complete_Sig.
+- now apply complete_Id.
 Qed.
 
 Lemma neuTerm {l wl Γ A} (RA : [Γ ||-<l> A]< wl >) {n} :
-  Ne[Γ |- n : A]< wl > ->
   [Γ |- n : A]< wl > ->
   [Γ |- n ~ n : A]< wl > ->
   [Γ ||-<l> n : A | RA]< wl >.
@@ -676,8 +602,6 @@ Proof.
 Qed.
 
 Lemma neuTermEq {l wl Γ A} (RA : [Γ ||-<l> A]< wl >) {n n'} :
-  Ne[Γ |- n : A]< wl > ->
-  Ne[Γ |- n' : A]< wl > ->
   [Γ |- n : A]< wl > ->
   [Γ |- n' : A]< wl > ->
   [Γ |- n ~ n' : A]< wl > ->
@@ -703,19 +627,7 @@ Proof.
   apply var0conv.
   rewrite eq.
   unshelve eapply escapeEq; tea.
-  eapply LRTyEqRefl_.
-Qed.
-
-Lemma reifyTerm {l wl Γ A} (RA : [Γ ||-<l> A]< wl >) {t} : [Γ ||-<l> t : A | RA]< wl > -> Nf[Γ |- t : A]< wl >.
-Proof.
-intros; now eapply completeness.
+  eapply reflLRTyEq.
 Qed.
 
-Lemma reifyType {l wl Γ A} (RA : [Γ ||-<l> A]< wl >) : Nf[Γ |- A]< wl >.
-Proof.
-  unshelve eapply reifyTyConv; tea.
-  1: now eapply completeness.
-  apply LRTyEqRefl_.
-Qed.
-*)
 End Neutral.
diff --git a/theories/LogicalRelation/NormalRed.v b/theories/LogicalRelation/NormalRed.v
index 4fc16a8..5ba66a0 100644
--- a/theories/LogicalRelation/NormalRed.v
+++ b/theories/LogicalRelation/NormalRed.v
@@ -1,126 +1,146 @@
 
+From Coq Require Import CRelationClasses.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations LContexts Context NormalForms Weakening GenericTyping LogicalRelation DeclarativeInstance.
+From LogRel Require Import Utils BasicAst Notations LContexts Context NormalForms UntypedReduction Weakening GenericTyping Monad LogicalRelation.
 From LogRel.LogicalRelation Require Import Induction Irrelevance Escape Reflexivity Weakening Neutral Transitivity Reduction.
 
 Set Universe Polymorphism.
 
+Ltac redSubst :=
+  match goal with
+  | [H : [_ |- ?X :⤳*: ?Y]< _ > |- _] => 
+    assert (X = Y)by (eapply redtywf_whnf ; gen_typing); subst; clear H
+  end.
+
+
 Section Normalization.
 Context `{GenericTypingProperties}.
 
 Set Printing Primitive Projection Parameters.
 
+
+Program Definition normRedNe0 {wl Γ A} (h : [Γ ||-ne A]< wl >) (wh : whne A) :
+  [Γ ||-ne A]< wl > :=
+  {| neRedTy.ty := A |}.
+Next Obligation.
+  pose proof (LRne_ zero h); escape; now eapply redtywf_refl.
+Qed.
+Next Obligation. destruct h; now redSubst. Qed.
+
+
+
 Program Definition normRedΠ0 {wl Γ F G l} (h : [Γ ||-Π<l> tProd F G]< wl >)
   : [Γ ||-Π<l> tProd F G]< wl > :=
   {| PiRedTyPack.dom := F ;
-    PiRedTyPack.cod := G |}.
-Obligation 1.
-  intros;
-  assert (wΠ : whnf (tProd F G)) by constructor;
-  pose proof (e := redtywf_whnf (PiRedTyPack.red h) wΠ);
-  symmetry in e; injection e; clear e.
-  destruct h as [?????? domRed codRed codExt] ; 
-    intros; cbn in *; subst; eassumption + now eapply domRed.
-Defined. 
-Obligation 2.
-  intros;
-  assert (wΠ : whnf (tProd F G)) by constructor;
-  pose proof (e := redtywf_whnf (PiRedTyPack.red h) wΠ);
-  symmetry in e; injection e; clear e.
-  destruct h as [?????? domRed codRed codExt] ; 
-    intros; cbn in *; subst; eassumption + now eapply domRed.
-Defined.
-Obligation 3.
-
-  intros;
-  assert (wΠ : whnf (tProd F G)) by constructor;
-  pose proof (e := redtywf_whnf (PiRedTyPack.red h) wΠ);
-  symmetry in e; injection e; clear e.
-  destruct h as [?????? domRed codRed codExt] ; 
-    intros; cbn in *; subst; eassumption + now eapply domRed.
-Defined.
-Obligation 4.
-  intros;
-  assert (wΠ : whnf (tProd F G)) by constructor;
-  pose proof (e := redtywf_whnf (PiRedTyPack.red h) wΠ);
-  symmetry in e; injection e; clear e.
-  destruct h as [?????? domRed codRed codExt] ; 
-    intros; cbn in *; subst; eassumption + now eapply domRed.
-Defined.
-Obligation 5.
-  destruct h as [??????? domRed codRed codExt] ; 
-    intros; cbn in *; subst. exact domN.
-Defined.
-Obligation 6. 
-  intros;
-  assert (wΠ : whnf (tProd F G)) by constructor;
-  pose proof (e := redtywf_whnf (PiRedTyPack.red h) wΠ);
-  symmetry in e; injection e; clear e.
-  destruct h as [??????? domRed codRed codExt] ; 
-    intros; cbn in *; subst; try eassumption.
-  eapply domRed ; try eassumption.
-Defined.
-Obligation 7.
-  intros;
-  assert (wΠ : whnf (tProd F G)) by constructor;
-  pose proof (e := redtywf_whnf (PiRedTyPack.red h) wΠ);
-  symmetry in e; injection e; clear e.
-  destruct h as [??????? domRed codomN codRed codExt].
-  intros ; cbn in *.
-  unshelve eapply codomN ; try eassumption.
-  subst.
-  now irrelevance.
-Defined.
+     PiRedTyPack.cod := G |}.
+Solve All Obligations with 
+  intros; pose proof (e := redtywf_whnf (PiRedTyPack.red h) whnf_tProd);
+  symmetry in e; injection e; clear e; 
+  destruct h ; intros; cbn in *; subst; eassumption.
 
-Obligation 8.
-  intros;
-  assert (wΠ : whnf (tProd F G)) by constructor.
-  pose proof (e := redtywf_whnf (PiRedTyPack.red h) wΠ).
-  symmetry in e; injection e; clear e.
-  destruct h as [??????? domRed codomN codRed codExt] ; 
-    intros; cbn in *.
-  subst.
-  unshelve eapply codRed ;[exact wl' |..] ; tea.
-Defined.
-
-Next Obligation.
-  intros;
-  assert (wΠ : whnf (tProd F G)) by constructor.
-  pose proof (e := redtywf_whnf (PiRedTyPack.red h) wΠ).
-  symmetry in e; injection e; clear e.
-  destruct h as [??????? domRed codomN codRed codExt] ; 
-    intros; cbn in *.
-  subst.
-  irrelevance0 ; try reflexivity.
-  unshelve eapply codExt ; [exact wl' | ..] ; try eassumption ; tea ; irrelevance.
-Qed.
 
+Program Definition normRedΣ0 {wl Γ F G l} (h : [Γ ||-Σ<l> tSig F G]< wl >)
+  : [Γ ||-Σ<l> tSig F G]< wl > :=
+  {| PiRedTyPack.dom := F ;
+     PiRedTyPack.cod := G |}.
+Solve All Obligations with 
+  intros; pose proof (e := redtywf_whnf (PiRedTyPack.red h) whnf_tSig);
+  symmetry in e; injection e; clear e; 
+  destruct h ; intros; cbn in *; subst; eassumption.
   
 Definition normRedΠ {wl Γ F G l} (h : [Γ ||-<l> tProd F G]< wl >)
   : [Γ ||-<l> tProd F G]< wl > :=
   LRPi' (normRedΠ0 (invLRΠ h)).
 
+
+Definition normRedΣ {wl Γ F G l} (h : [Γ ||-<l> tSig F G]< wl >) : [Γ ||-<l> tSig F G]< wl > :=
+  LRSig' (normRedΣ0 (invLRΣ h)).
+
+#[program]
+Definition normEqRedΣ {wl Γ F F' G G' l} (h : [Γ ||-<l> tSig F G]< wl >) 
+  (heq : [Γ ||-<l> _ ≅ tSig F' G' | h]< wl >) : [Γ ||-<l> _ ≅ tSig F' G' | normRedΣ h]< wl > :=
+  {|
+    PiRedTyEq.dom := F';
+    PiRedTyEq.cod := G';
+  |}.
+Solve All Obligations with
+  intros; assert[Γ ||-<l> _ ≅ tSig F' G' | normRedΣ h]< wl > as [?? red] by irrelevance;
+  pose proof (e := redtywf_whnf red whnf_tSig);
+  symmetry in e; injection e; clear e; 
+  destruct h ; intros; cbn in *; subst; eassumption.
+
 #[program]
 Definition normLambda {wl Γ F F' G t l RΠ} 
   (Rlam : [Γ ||-<l> tLambda F' t : tProd F G | normRedΠ RΠ ]< wl >) :
   [Γ ||-<l> tLambda F' t : tProd F G | normRedΠ RΠ ]< wl > :=
   {| PiRedTm.nf := tLambda F' t |}.
+Obligation 3.
+eapply (PiRedTm.appTree Rlam ρ f Hd ha).
+Defined.
 Obligation 5.
-  destruct Rlam as [??????? app eqq]; cbn in *; try exact redN.
+pose proof (e := redtmwf_whnf (PiRedTm.red Rlam) whnf_tLambda).
+destruct Rlam as [????? app eqq].
+eapply (f_equal (ren_term ρ)) in e ; cbn in *.
+rewrite e.
+now eapply app.
 Defined.
-Obligation 6.
+Solve All Obligations with
   intros;
   pose proof (e := redtmwf_whnf (PiRedTm.red Rlam) whnf_tLambda);
-    destruct Rlam as [??????? app eqq]; cbn in *.
-  unshelve eapply appN ; try eassumption ; subst ; try eassumption.
-Defined.
+  destruct Rlam as [????? app eqq]; cbn in *; subst;
+first [eapply app | now eapply eqq| eassumption].
 
-Solve All Obligations with
+
+#[program]
+Definition normPair {wl Γ F F' G G' f g l RΣ} 
+  (Rp : [Γ ||-<l> tPair F' G' f g : tSig F G | normRedΣ RΣ ]< wl >) :
+  [Γ ||-<l> tPair F' G' f g : tSig F G | normRedΣ RΣ ]< wl > :=
+  {| SigRedTm.nf := tPair F' G' f g |}.
+Obligation 4.
+eapply (SigRedTm.sndTree Rp) ; eassumption.
+Defined.
+Obligation 5.
   intros;
-  pose proof (e := redtmwf_whnf (PiRedTm.red Rlam) whnf_tLambda);
-  destruct Rlam as [??????? app eqq]; cbn in *; try exact redN ; subst;
-first [eapply app ; eassumption | now eapply eqq| eassumption].
-  
+  pose proof (e := redtmwf_whnf (SigRedTm.red Rp) whnf_tPair);
+    destruct Rp as [??? fstRed ?? sndRed]; cbn in * ; now subst.
+Defined.
+Next Obligation.
+  intros;
+    pose proof (e := redtmwf_whnf (SigRedTm.red Rp) whnf_tPair);
+    destruct Rp as [??? fstRed ?? sndRed]; cbn in *; now subst.
+Defined.
+Next Obligation.
+  intros;
+    pose proof (e := redtmwf_whnf (SigRedTm.red Rp) whnf_tPair);
+    destruct Rp as [??? fstRed ?? sndRed]; cbn in *; now subst.
+Defined.
+Next Obligation.
+  intros;
+    pose proof (e := redtmwf_whnf (SigRedTm.red Rp) whnf_tPair);
+    destruct Rp as [??? fstRed ?? sndRed]; cbn in *; subst.
+  now eapply fstRed.
+Defined.
+Next Obligation.
+  intros;
+    destruct Rp as [??? fstRed ?? sndRed]; cbn in *.
+  unfold normPair_obligation_3 in * ; cbn in * ; revert Ho.
+  destruct (redtmwf_whnf red whnf_tPair) ; subst ; cbn in *.
+  intros Ho.
+  irrelevanceRefl ; unshelve eapply sndRed.
+  4,5: eassumption.
+Defined.
+
+Definition invLRcan {wl Γ l A} (lr : [Γ ||-<l> A]< wl >) (w : isType A) : [Γ ||-<l> A]< wl > :=
+  match w as w in isType A return forall (lr : [Γ ||-<l> A]< wl >), invLRTy lr (reflexivity A) w -> [Γ ||-<l> A]< wl > with
+  | UnivType => fun _ x => LRU_ x
+  | ProdType => fun _ x => LRPi' (normRedΠ0 x)
+  | NatType => fun _ x => LRNat_ _ x
+  | BoolType => fun _ x => LRBool_ _ x
+  | EmptyType => fun _ x => LREmpty_  _ x
+  | SigType => fun _ x => LRSig' (normRedΣ0 x)
+  | IdType => fun _ x => LRId' x
+  | NeType wh => fun _ x => LRne_ _ (normRedNe0 x wh)
+  end lr (invLR lr (reflexivity A) w).
 
 End Normalization.
 
@@ -128,20 +148,33 @@ End Normalization.
 
 (* Normalizes a term reducible at a Π type *)
 
-Ltac normRedΠin id X :=
+Ltac normRedΠin X :=
   let g := type of X in
   match g with
   | [ LRAd.pack ?R | _ ||- ?t : _]< _ > =>
-    pose (id := normRedΠ0 (invLRΠ R));
     let X' := fresh X in
     rename X into X' ;
-    assert (X : [_ ||-<_> t : _ | LRPi' id]< _ >) by irrelevance; clear X'
+    assert (X : [_ ||-<_> t : _ | LRPi' (normRedΠ0 (invLRΠ R))]< _ >) by irrelevance; clear X'
+  | [ LRAd.pack ?R | _ ||- _ ≅ ?B]< _ > =>
+    let X' := fresh X in
+    rename X into X' ;
+    assert (X : [_ ||-<_> _ ≅ B | LRPi' (normRedΠ0 (invLRΠ R))]< _ >) by irrelevance; clear X'
+  | [ LRAd.pack ?R | _ ||- ?t ≅ ?u : _]< _ > =>
+    let X' := fresh X in
+    rename X into X' ;
+    assert (X : [_ ||-<_> t ≅ u : _ | LRPi' (normRedΠ0 (invLRΠ R))]< _ >) by irrelevance; clear X'
   end.
 
-Goal forall `{GenericTypingProperties} wl Γ A B l R f (Rf : [Γ ||-<l> f : arr A B | R]< wl >), True.
+Goal forall `{GenericTypingProperties} wl Γ A B l R f X
+  (RABX : [Γ ||-<l> arr A B ≅ X | R]< wl >)
+  (Rf : [Γ ||-<l> f : arr A B | R]< wl >)
+  (Rff : [Γ ||-<l> f ≅ f : arr A B | R]< wl >)
+, True.
 Proof.
   intros.
-  normRedΠin ΠAB Rf.
+  normRedΠin Rf.
+  normRedΠin Rff.
+  normRedΠin RABX.
   constructor.
 Qed.
 
@@ -157,3 +190,22 @@ Ltac normRedΠ id :=
     enough [_ ||-<_> t : _ | LRPi' id]< _ > by irrelevance
   end.
 
+(* Normalizes a term reducible at a Π type *)
+
+Ltac normRedΣin X :=
+  let g := type of X in
+  match g with
+  | [ LRAd.pack ?R | _ ||- ?t : _]< _ > =>
+    let X' := fresh X in
+    rename X into X' ;
+    assert (X : [_ ||-<_> t : _ | LRSig' (normRedΣ0 (invLRΣ R))]< _ >) by irrelevance; clear X'
+  | [ LRAd.pack ?R | _ ||- _ ≅ ?B]< _ > =>
+    let X' := fresh X in
+    rename X into X' ;
+    assert (X : [_ ||-<_> _ ≅ B | LRSig' (normRedΣ0 (invLRΣ R))]< _ >) by irrelevance; clear X'
+  | [ LRAd.pack ?R | _ ||- ?t ≅ ?u : _]< _ > =>
+    let X' := fresh X in
+    rename X into X' ;
+    assert (X : [_ ||-<_> t ≅ u : _ | LRSig' (normRedΣ0 (invLRΣ R))]< _ >) by irrelevance; clear X'
+  end.
+
diff --git a/theories/LogicalRelation/Reduction.v b/theories/LogicalRelation/Reduction.v
index b6311d5..689213f 100644
--- a/theories/LogicalRelation/Reduction.v
+++ b/theories/LogicalRelation/Reduction.v
@@ -1,6 +1,6 @@
 (* From Coq.Classes Require Import CRelationClasses. *)
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Notations Utils BasicAst LContexts Context NormalForms UntypedReduction Weakening GenericTyping LogicalRelation DeclarativeInstance.
+From LogRel Require Import Notations Utils BasicAst LContexts Context NormalForms UntypedReduction Weakening GenericTyping Monad LogicalRelation DeclarativeInstance.
 From LogRel.LogicalRelation Require Import Induction Reflexivity Universe Escape Irrelevance.
 
 Set Universe Polymorphism.
@@ -12,7 +12,7 @@ Set Printing Primitive Projection Parameters.
 
 Lemma redSubst {wl Γ A B l} :
   [Γ ||-<l> B]< wl > ->
-  [Γ |- A ⇒* B]< wl > ->
+  [Γ |- A ⤳* B]< wl > ->
   ∑ (RA : [Γ ||-<l> A]< wl >), [Γ ||-<l> A ≅ B | RA]< wl >.
 Proof.
   intros RB; revert A; pattern l, wl, Γ, B, RB; apply LR_rect_TyUr; clear l wl Γ B RB; intros l wl Γ.
@@ -25,13 +25,12 @@ Proof.
       constructor; tea; gen_typing.
     + exists t; tea.
   - intros B [dom cod] A ? ihdom ihcod; cbn in *; unshelve eexists.
-    + apply LRPi'; unshelve eexists dom cod _ _ _ _; tea; etransitivity; tea.
+    + apply LRPi'; unshelve eexists dom cod ; tea; etransitivity; tea.
       constructor; tea; gen_typing.
-    + unshelve eexists dom cod _ _; tea; cbn.
-      2,3: intros; apply LRTyEqRefl_.
-      intros ; unshelve eapply codomN.
-      6: exact Ninfl.
-      all: try assumption.
+    + unshelve eexists dom cod ; tea; cbn.
+      unshelve econstructor;intros.
+      2,3: apply reflLRTyEq.
+      now eapply leaf.
   - intros B [red] A ?; unshelve eexists.
     + apply LRNat_; constructor; tea; etransitivity; tea.
       constructor; tea; gen_typing.
@@ -44,28 +43,39 @@ Proof.
     + apply LREmpty_; constructor; tea; etransitivity; tea.
       constructor; tea; gen_typing.
     + now constructor.
+  - intros B [dom cod] A ? ihdom ihcod; cbn in *; unshelve eexists.
+    + apply LRSig'; unshelve eexists dom cod; tea; etransitivity; tea.
+      constructor; tea; gen_typing.
+    + unshelve eexists dom cod; tea; cbn.
+      unshelve econstructor;intros; try now apply reflLRTyEq.
+      now eapply leaf.
+  - intros ? [ty lhs rhs] ih _ X redX; unshelve eexists.
+    + apply LRId'; unshelve eexists ty lhs rhs _ _; tea.
+      etransitivity; tea; constructor; tea; gen_typing.
+    + exists ty lhs rhs; tea; eapply reflLRTyEq.
 Qed.
 
 Lemma WredSubst {wl Γ A B l} :
   W[Γ ||-<l> B]< wl > ->
-  [Γ |- A ⇒* B]< wl > ->
+  [Γ |- A ⤳* B]< wl > ->
   ∑ (RA : W[Γ ||-<l> A]< wl >), W[Γ ||-<l> A ≅ B | RA]< wl >.
 Proof.
   intros [] ?.
   unshelve econstructor.
-  - exists WN.
+  - exists WT.
     intros.
     eapply redSubst.
     + eapply WRed ; try assumption.
-    + now eapply redty_Ltrans.
-  - exists WN.
+    + eapply redty_Ltrans ; eauto.
+      now eapply over_tree_le.
+  - exists WT.
     cbn ; intros.
-    now destruct (redSubst (WRed wl' τ Ninfl) (redty_Ltrans τ H14)).
+    now destruct (redSubst (WRed wl' Hover) (redty_Ltrans (over_tree_le Hover) H10)).
 Qed.   
     
 Lemma redwfSubst {wl Γ A B l} :
   [Γ ||-<l> B]< wl > ->
-  [Γ |- A :⇒*: B]< wl > ->
+  [Γ |- A :⤳*: B]< wl > ->
   ∑ (RA : [Γ ||-<l> A]< wl >), [Γ ||-<l> A ≅ B | RA]< wl >.
 Proof.
   intros ? []; now eapply redSubst.
@@ -73,14 +83,14 @@ Qed.
 
 Lemma redSubstTerm {wl Γ A t u l} (RA : [Γ ||-<l> A]< wl >) :
   [Γ ||-<l> u : A | RA]< wl > ->
-  [Γ |- t ⇒* u : A ]< wl > ->
+  [Γ |- t ⤳* u : A ]< wl > ->
   [Γ ||-<l> t : A | RA]< wl > × [Γ ||-<l> t ≅ u : A | RA]< wl >.
 Proof.
   revert t u; pattern l, wl, Γ, A, RA; apply LR_rect_TyUr; clear l wl Γ A RA; intros l wl Γ.
   - intros ? h ?? ru' redtu; pose (ru := ru'); destruct ru' as [T].
     assert [Γ |- A ≅ U]< wl > by (destruct h; gen_typing).
     assert [Γ |- t : U]< wl > by (eapply ty_conv; [gen_typing| now escape]).
-    assert (redtu' : [Γ |-[ ta ] t ⇒* u]< wl >) by gen_typing.
+    assert (redtu' : [Γ |-[ ta ] t ⤳* u]< wl >) by gen_typing.
     destruct (redSubst (A:=t) (RedTyRecFwd h rel) redtu') as [rTyt0].
     pose proof (rTyt := RedTyRecBwd h rTyt0).
     unshelve refine (let rt : [LRU_ h | Γ ||- t : A]< wl >:= _ in _).
@@ -93,30 +103,31 @@ Proof.
       destruct neA; cbn in *.
       eapply convty_exp.
        2: apply redtywf_refl; gen_typing.
-       2: apply convty_term; now apply convtm_convneu.
+       2: apply convty_term, convtm_convneu ; eauto.
        gen_typing.
+       now constructor.
     }
-    assert [Γ |-[ ta ] t ⇒* u : neRedTy.ty neA]< wl > by (eapply redtm_conv; tea). 
+    assert [Γ |-[ ta ] t ⤳* u : neRedTy.ty neA]< wl > by (eapply redtm_conv; tea). 
     assert [Γ |-[ ta ] t : neRedTy.ty neA]< wl > by (eapply ty_conv; tea; gen_typing). 
     unshelve refine (let rt : [LRne_ l neA | Γ ||- t : A]< wl > := _ in _).
     + exists n; tea; destruct red; constructor; tea; now etransitivity.
     + split; tea; exists n n; tea; destruct red; constructor; tea; now etransitivity. 
   - intros ? ΠA ihdom ihcod ?? ru' ?; pose (ru := ru'); destruct ru' as [f].
-    assert [Γ |- A ≅ PiRedTyPack.prod ΠA]< wl >. 1:{
+    assert [Γ |- A ≅ ΠA.(outTy)]< wl >. 1:{
       destruct ΠA as [?? []]. cbn in *.
       eapply convty_exp; tea.
       now apply redtywf_refl.
     }
-    assert [Γ |-[ ta ] t ⇒* u : PiRedTyPack.prod ΠA]< wl > by now eapply redtm_conv. 
-    assert [Γ |-[ ta ] t : PiRedTyPack.prod ΠA]< wl > by (eapply ty_conv; gen_typing).
+    assert [Γ |-[ ta ] t ⤳* u : ΠA.(outTy)]< wl > by now eapply redtm_conv. 
+    assert [Γ |-[ ta ] t : ΠA.(outTy)]< wl > by (eapply ty_conv; gen_typing).
     unshelve refine (let rt : [LRPi' ΠA | Γ ||- t : A]< wl > := _ in _).
-    1: exists f redN appN ; tea ; constructor ; destruct red ; tea ; etransitivity ; tea.
+    1: exists f appTree ; tea ; constructor ; destruct red ; tea ; etransitivity ; tea.
     split; tea; unshelve eexists ; tea.
     intros; cbn. eapply eq; tea.
-    now apply LREqTermRefl_.
+    now apply reflLRTmEq.
   - intros ? NA t ? Ru red; inversion Ru; subst.
     assert [Γ |- A ≅ tNat]< wl > by (destruct NA; gen_typing).
-    assert [Γ |- t :⇒*: nf : tNat]< wl >. 1:{
+    assert [Γ |- t :⤳*: nf : tNat]< wl >. 1:{
       constructor. 1: gen_typing.
       etransitivity. 2: gen_typing.
       now eapply redtm_conv.
@@ -125,7 +136,7 @@ Proof.
     now eapply reflNatRedTmEq.
   - intros ? NA t ? Ru red; inversion Ru; subst.
     assert [Γ |- A ≅ tBool]< wl > by (destruct NA; gen_typing).
-    assert [Γ |- t :⇒*: nf : tBool]< wl >. 1:{
+    assert [Γ |- t :⤳*: nf : tBool]< wl >. 1:{
       constructor. 
       1: eapply ty_conv; gen_typing.
       etransitivity. 2: gen_typing.
@@ -135,7 +146,7 @@ Proof.
     now eapply reflBoolRedTmEq.
   - intros ? NA t ? Ru red; inversion Ru; subst.
     assert [Γ |- A ≅ tEmpty]< wl > by (destruct NA; gen_typing).
-    assert [Γ |- t :⇒*: nf : tEmpty]< wl >. 1:{
+    assert [Γ |- t :⤳*: nf : tEmpty]< wl >. 1:{
       constructor. 
       1: eapply ty_conv; gen_typing.
       etransitivity. 2: gen_typing.
@@ -144,29 +155,43 @@ Proof.
     split; econstructor; tea.
     now eapply reflEmptyRedTmEq.
     Unshelve. 2: tea.
+  - intros ? PA ihdom ihcod ?? ru' ?; pose (ru := ru'); destruct ru' as [p].
+    assert [Γ |- A ≅ PA.(outTy)]< wl >. 1:{
+      destruct PA as [?? []]. cbn in *.
+      eapply convty_exp; tea.
+      now apply redtywf_refl.
+    }
+    assert [Γ |-[ ta ] t ⤳* u : PA.(outTy)]< wl > by now eapply redtm_conv. 
+    assert [Γ |-[ ta ] t : PA.(outTy)]< wl > by (eapply ty_conv; gen_typing).
+    unshelve refine (let rt : [LRSig' PA | Γ ||- t : A]< wl > := _ in _).
+    1: unshelve eexists p _ _; tea; constructor; destruct red; tea; etransitivity; tea.
+    split; tea; exists rt ru sndTree; tea; intros; cbn; now apply reflLRTmEq.
+  - intros ? IA ih _ t u [nf ?? prop] redt.
+    assert [Γ |- A ≅ IA.(IdRedTy.outTy)]< wl > by (destruct IA; unfold IdRedTy.outTy; cbn; gen_typing).
+    assert [Γ |-[ ta ] t ⤳* u : IA.(IdRedTy.outTy)]< wl > by now eapply redtm_conv. 
+    assert [Γ |-[ ta ] t : IA.(IdRedTy.outTy)]< wl > by (eapply ty_conv; gen_typing).
+    assert [Γ |-[ ta ] t :⤳*: nf : IA.(IdRedTy.outTy)]< wl >.
+    1: constructor; [apply red|etransitivity; tea; apply red].
+    split; eexists; tea.
+    now eapply reflIdPropEq.
 Qed.
 
 Lemma WredSubstTerm {wl Γ A t u l}
   (RA : W[Γ ||-<l> A]< wl >) :
   W[Γ ||-<l> u : A | RA]< wl > ->
-  [Γ |- t ⇒* u : A ]< wl > ->
+  [Γ |- t ⤳* u : A ]< wl > ->
   W[Γ ||-<l> t : A | RA]< wl > × W[Γ ||-<l> t ≅ u : A | RA]< wl >.
 Proof.
   intros [] ?.
-  split ; exists WNTm.
-  - intros.
-    eapply redSubstTerm.
-    + now eapply WRedTm.
-    + now eapply redtm_Ltrans.
-  - intros.
-    eapply redSubstTerm.
-    + now eapply WRedTm.
-    + now eapply redtm_Ltrans.
+  split ; exists WTTm ; intros.
+  all: pose proof (Hyp := over_tree_le Hover).
+  all: eapply redSubstTerm ; [now eapply WRedTm | ].
+  all: now eapply redtm_Ltrans.
 Qed.
 
 Lemma redwfSubstTerm {wl Γ A t u l} (RA : [Γ ||-<l> A]< wl >) :
   [Γ ||-<l> u : A | RA]< wl > ->
-  [Γ |- t :⇒*: u : A ]< wl > ->
+  [Γ |- t :⤳*: u : A ]< wl > ->
   [Γ ||-<l> t : A | RA]< wl > × [Γ ||-<l> t ≅ u : A | RA]< wl >.
 Proof.
   intros ? []; now eapply redSubstTerm.
@@ -175,54 +200,70 @@ Qed.
 
 Lemma redFwd {wl Γ l A B} :
   [Γ ||-<l> A]< wl > ->
-  [Γ |- A :⇒*: B]< wl > ->
+  [Γ |- A :⤳*: B]< wl > ->
   whnf B ->
   [Γ ||-<l> B]< wl >.
 Proof.
   intros RA; revert B; pattern l, wl, Γ, A, RA; apply LR_rect_TyUr; clear l wl Γ A RA.
   - intros ???? [??? red] ? red' ?. 
-    eapply LRU_.  unshelve erewrite (redtywf_det _ _ _ _ _ _ _ red' red); tea.
+    eapply LRU_.  unshelve erewrite (redtywf_det _ _ red' red); tea.
     1: constructor. econstructor; tea. eapply redtywf_refl; gen_typing.
   - intros ???? [? red] ? red' ?.
     eapply LRne_.
-    unshelve erewrite (redtywf_det _ _ _ _ _ _ _ red' red); tea.
-    1: constructor; now eapply ty_ne_whne.
+    unshelve erewrite (redtywf_det _ _ red' red); tea.
+    1: constructor; now eapply convneu_whne.
     econstructor; tea.
     eapply redtywf_refl; gen_typing.
   - intros ???? [?? red] ?? ? red' ?.
     eapply LRPi'. 
-    unshelve erewrite (redtywf_det _ _ _ _ _ _ _ red' red); tea.
+    unshelve erewrite (redtywf_det _ _ red' red); tea.
     1: constructor.
-    econstructor; tea.
-    eapply redtywf_refl; gen_typing.
+    econstructor.
+    + eapply redtywf_refl; gen_typing.
+    + eassumption.
+    + eassumption.
+    + eassumption.
   - intros ???? [red] ? red' ?.
     eapply LRNat_.
-    unshelve erewrite (redtywf_det _ _ _ _ _ _ _ red' red); tea.
+    unshelve erewrite (redtywf_det _ _ red' red); tea.
     1: constructor.
     econstructor; tea.
     eapply redtywf_refl; gen_typing.
   - intros ???? [red] ? red' ?.
     eapply LRBool_.
-    unshelve erewrite (redtywf_det _ _ _ _ _ _ _ red' red); tea.
+    unshelve erewrite (redtywf_det _ _ red' red); tea.
     1: constructor.
     econstructor; tea.
     eapply redtywf_refl; gen_typing.
   - intros ???? [red] ? red' ?.
     eapply LREmpty_.
-    unshelve erewrite (redtywf_det _ _ _ _ _ _ _ red' red); tea.
+    unshelve erewrite (redtywf_det _ _ red' red); tea.
     1: constructor.
     econstructor; tea.
     eapply redtywf_refl; gen_typing.
+  - intros ???? [?? red] ?? ? red' ?.
+    eapply LRSig'. 
+    unshelve erewrite (redtywf_det _ _ red' red); tea.
+    1: constructor.
+    econstructor.
+    + eapply redtywf_refl; gen_typing.
+    + eassumption.
+    + eassumption.
+    + eassumption.
+  - intros ???? [???? red] _ _ ? red' ?.
+    eapply LRId'; unshelve erewrite (redtywf_det _ _ red' red); tea; [constructor|].
+    econstructor; tea. eapply redtywf_refl; gen_typing.
 Qed.
 
 Lemma WredFwd {wl Γ l A B} :
   W[Γ ||-<l> A]< wl > ->
-  [Γ |- A :⇒*: B]< wl > ->
+  [Γ |- A :⤳*: B]< wl > ->
   whnf B ->
   W[Γ ||-<l> B]< wl >.
 Proof.
   intros [] red whB.
-  exists WN ; intros.
+  exists WT ; intros.
+  pose proof (Hyp := over_tree_le Ho).
   unshelve eapply redFwd.
   - exact A.
   - now eapply WRed.
@@ -233,15 +274,26 @@ Proof.
 Qed.
 
 
+Lemma redFwdConv {wl Γ l A B} (RA : [Γ ||-<l> A]< wl >) : [Γ |- A :⤳*: B]< wl > -> whnf B -> [Γ ||-<l> B]< wl > × [Γ ||-<l> A ≅ B | RA]< wl >.
+Proof.
+  intros red wh. pose (RB := redFwd RA red wh).
+  destruct (redwfSubst RB red).
+  split; tea; irrelevance.
+Qed.
+
+Lemma IdProp_whnf {wl Γ l A} (IA : [Γ ||-Id<l> A]< wl >) t : IdProp IA t -> whnf t.
+Proof. intros []; constructor; destruct r; now eapply convneu_whne. Qed.
+
+
 Lemma redTmFwd {wl Γ l A t u} {RA : [Γ ||-<l> A]< wl >} : 
   [Γ ||-<l> t : A | RA]< wl > ->
-  [Γ |- t :⇒*: u : A]< wl > ->
+  [Γ |- t :⤳*: u : A]< wl > ->
   whnf u ->
   [Γ ||-<l> u : A | RA]< wl >.
 Proof.
   revert t u; pattern l,wl, Γ,A,RA; apply LR_rect_TyUr; clear l wl Γ A RA.
   - intros ??????? [? red] red' ?.
-    unshelve erewrite (redtmwf_det _ _ _ _ _ _ _ _ _ red' red); tea.
+    unshelve erewrite (redtmwf_det _ _ red' red); tea.
     1: now eapply isType_whnf.
     econstructor; tea.
     1: eapply redtmwf_refl; gen_typing.
@@ -249,41 +301,52 @@ Proof.
     2,3: gen_typing.
     now eapply RedTyRecFwd.
   - intros ???? ??? [? red] red' ?.
-    unshelve erewrite (redtmwf_det _ _ _ _ _ _ _ _ _ red' red); tea.
-    1: constructor; now eapply tm_ne_whne.
+    unshelve erewrite (redtmwf_det _ _ red' red); tea.
+    1: constructor; now eapply convneu_whne.
     econstructor; tea.
     eapply redtmwf_refl; gen_typing.
   - intros ????????? [? red] red' ?.
-    unshelve erewrite (redtmwf_det _ _ _ _ _ _ _ _ _ red' red); tea.
-    1: now eapply isFun_whnf.
+    unshelve erewrite (redtmwf_det _ _ red' red); tea.
+    1: eapply isFun_whnf; destruct isfun; constructor; tea; now eapply convneu_whne.
     econstructor; tea.
     eapply redtmwf_refl; gen_typing.
   - intros ??????? Rt red' ?; inversion Rt; subst.
-    unshelve erewrite (redtmwf_det _ _ _ _ _ _ _ _ _ red' red); tea.
+    unshelve erewrite (redtmwf_det _ _ red' red); tea.
     1: now eapply NatProp_whnf.
     econstructor; tea.
     eapply redtmwf_refl; gen_typing.
   - intros ??????? Rt red' ?; inversion Rt; subst.
-    unshelve erewrite (redtmwf_det _ _ _ _ _ _ _ _ _ red' red); tea.
+    unshelve erewrite (redtmwf_det _ _ red' red); tea.
     1: now eapply BoolProp_whnf.
     econstructor; tea.
     eapply redtmwf_refl; gen_typing.
   - intros ??????? Rt red' ?; inversion Rt; subst.
-    unshelve erewrite (redtmwf_det _ _ _ _ _ _ _ _ _ red' red); tea.
+    unshelve erewrite (redtmwf_det _ _ red' red); tea.
     1: now eapply EmptyProp_whnf.
     econstructor; tea.
     eapply redtmwf_refl; gen_typing.
     Unshelve. 2: tea.
+  - intros ????????? [? red] red' ?.
+    unshelve erewrite (redtmwf_det _ _ red' red); tea.
+    1: eapply isPair_whnf; destruct ispair; constructor; tea; now eapply convneu_whne.
+    econstructor; tea.
+    eapply redtmwf_refl; gen_typing.
+  - intros ????????? [? red] red' ?.
+    unshelve erewrite (redtmwf_det _ _ red' red); tea.
+    1: now eapply IdProp_whnf.
+    econstructor; tea.
+    eapply redtmwf_refl; gen_typing.
 Qed.
 
 Lemma WredTmFwd {wl Γ l A t u} {RA : W[Γ ||-<l> A]< wl >} : 
   W[Γ ||-<l> t : A | RA]< wl > ->
-  [Γ |- t :⇒*: u : A]< wl > ->
+  [Γ |- t :⤳*: u : A]< wl > ->
   whnf u ->
   W[Γ ||-<l> u : A | RA]< wl >.
 Proof.
   intros [] [wfA red] whu.
-  exists WNTm ; intros.
+  exists WTTm ; intros.
+  pose proof (Hyp := over_tree_le Hover).
   eapply redTmFwd ; try assumption.
   - now eapply WRedTm.
   - econstructor.
diff --git a/theories/LogicalRelation/Split.v b/theories/LogicalRelation/Split.v
new file mode 100644
index 0000000..d27706b
--- /dev/null
+++ b/theories/LogicalRelation/Split.v
@@ -0,0 +1,94 @@
+From LogRel.AutoSubst Require Import core unscoped Ast Extra.
+From LogRel Require Import Utils BasicAst Notations LContexts Context NormalForms Weakening GenericTyping Monad LogicalRelation.
+From LogRel.LogicalRelation Require Import Induction Irrelevance.
+
+Section Split.
+  Context `{GenericTypingProperties}.
+
+  Lemma Split@{i j k l} {wl : wfLCon} {lA Γ A} {n : nat} {ne : not_in_LCon wl n} :
+    WLogRel@{i j k l} lA (wl ,,l (ne, true)) Γ A ->
+    WLogRel@{i j k l} lA (wl ,,l (ne, false)) Γ A ->
+    WLogRel@{i j k l} lA wl Γ A.
+  Proof.
+    intros [WTt WRedt] [WTf WRedf].
+    exists (ϝnode _ WTt WTf).
+    intros wl' Hover.
+    cbn in *.
+    destruct (decidInLCon wl' n) ; [ | | now inversion Hover].
+    - now eapply WRedt.
+    - now eapply WRedf.
+  Defined.
+
+  Lemma EqSplit@{i j k l} {wl : wfLCon} {lA Γ A B} {n : nat} {ne : not_in_LCon wl n}
+    HAt HAf :
+    WLogRelEq@{i j k l} lA (wl ,,l (ne, true)) Γ A B HAt ->
+    WLogRelEq@{i j k l} lA (wl ,,l (ne, false)) Γ A B HAf ->
+    WLogRelEq@{i j k l} lA wl Γ A B (Split HAt HAf).
+  Proof.
+    intros [WTt WRedt] [WTf WRedf].
+    exists (ϝnode _ WTt WTf).
+    intros wl' Hover Hover' ; cbn in *.
+    destruct (decidInLCon wl' n) ; [ | | now inversion Hover].
+    - now eapply WRedt.
+    - now eapply WRedf.
+  Qed.
+
+  Corollary EqSplit'@{i j k l} {wl : wfLCon} {lA Γ A B} {n : nat} {ne : not_in_LCon wl n}
+    HAt HAf HA :
+    WLogRelEq@{i j k l} lA (wl ,,l (ne, true)) Γ A B HAt ->
+    WLogRelEq@{i j k l} lA (wl ,,l (ne, false)) Γ A B HAf ->
+    WLogRelEq@{i j k l} lA wl Γ A B HA.
+  Proof.
+    intros HBt HBf ; eapply WLRTyEqIrrelevant' ; [reflexivity | ].
+    eapply EqSplit ; eassumption.
+  Qed. 
+
+  Lemma TmSplit@{i j k l} {wl : wfLCon} {lA Γ t A} {n : nat} {ne : not_in_LCon wl n}
+    HAt HAf :
+    WLogRelTm@{i j k l} lA (wl ,,l (ne, true)) Γ t A HAt ->
+    WLogRelTm@{i j k l} lA (wl ,,l (ne, false)) Γ t A HAf ->
+    WLogRelTm@{i j k l} lA wl Γ t A (Split HAt HAf).
+  Proof.
+    intros [WTt WRedt] [WTf WRedf].
+    exists (ϝnode _ WTt WTf).
+    intros wl' Hover Hover' ; cbn in *.
+    destruct (decidInLCon wl' n) ; [ | | now inversion Hover].
+    - now eapply WRedt.
+    - now eapply WRedf.
+  Qed.
+
+  Corollary TmSplit'@{i j k l} {wl : wfLCon} {lA Γ t A} {n : nat} {ne : not_in_LCon wl n}
+    HAt HAf HA :
+    WLogRelTm@{i j k l} lA (wl ,,l (ne, true)) Γ t A HAt ->
+    WLogRelTm@{i j k l} lA (wl ,,l (ne, false)) Γ t A HAf ->
+    WLogRelTm@{i j k l} lA wl Γ t A HA.
+  Proof.
+    intros Htt Htf ; eapply WLRTmRedIrrelevant' ; [reflexivity | ].
+    eapply TmSplit ; eassumption.
+  Qed. 
+
+  Lemma TmEqSplit@{i j k l} {wl : wfLCon} {lA Γ t u A} {n : nat} {ne : not_in_LCon wl n}
+    HAt HAf :
+    WLogRelTmEq@{i j k l} lA (wl ,,l (ne, true)) Γ t u A HAt ->
+    WLogRelTmEq@{i j k l} lA (wl ,,l (ne, false)) Γ t u A HAf ->
+    WLogRelTmEq@{i j k l} lA wl Γ t u A (Split HAt HAf).
+  Proof.
+    intros [WTt WRedt] [WTf WRedf].
+    exists (ϝnode _ WTt WTf).
+    intros wl' Hover Hover' ; cbn in *.
+    destruct (decidInLCon wl' n) ; [ | | now inversion Hover].
+    - now eapply WRedt.
+    - now eapply WRedf.
+  Qed.
+
+  Lemma TmEqSplit'@{i j k l} {wl : wfLCon} {lA Γ t u A} {n : nat} {ne : not_in_LCon wl n}
+    HAt HAf HA :
+    WLogRelTmEq@{i j k l} lA (wl ,,l (ne, true)) Γ t u A HAt ->
+    WLogRelTmEq@{i j k l} lA (wl ,,l (ne, false)) Γ t u A HAf ->
+    WLogRelTmEq@{i j k l} lA wl Γ t u A HA.
+  Proof.
+    intros Htt Htf ; eapply WLRTmEqIrrelevant' ; [reflexivity | ].
+    eapply TmEqSplit ; eassumption.
+  Qed. 
+  
+End Split.
diff --git a/theories/LogicalRelation/Transitivity.v b/theories/LogicalRelation/Transitivity.v
index 0d79a9c..4ac851e 100644
--- a/theories/LogicalRelation/Transitivity.v
+++ b/theories/LogicalRelation/Transitivity.v
@@ -20,6 +20,14 @@ Set Printing Primitive Projection Parameters.
   [Γ ||-<lA> A ≅ C | RA]< wl >.
  Proof. now eapply LRTransEq. Qed.
 
+ Lemma WtransEq@{i j k l} {wl Γ A B C lA lB} 
+  {RA : WLogRel@{i j k l} lA wl Γ A }
+  {RB : WLogRel@{i j k l} lB wl Γ B }
+  (RAB : W[Γ ||-<lA> A ≅ B | RA]< wl >)
+   (RBC : W[Γ ||-<lB> B ≅ C | RB]< wl >) :
+  W[Γ ||-<lA> A ≅ C | RA]< wl >.
+ Proof. now eapply WLRTransEq. Qed.
+
 
 Lemma transEqTermU@{h i j k} {wl Γ l UU t u v} {h : [Γ ||-U<l> UU]< wl >} :
   [LogRelRec@{i j k} l | Γ ||-U t ≅ u : UU| h]< wl > ->
@@ -260,6 +268,18 @@ Proof.
   - intros; now eapply transTmEqId.
 Qed.
 
+Lemma WtransEqTerm@{h i j k l} {wl Γ lA A t u v} 
+  {RA : WLogRel@{i j k l} lA wl Γ A} :
+  W[Γ ||-<lA> t ≅ u : A | RA]< wl > ->
+  W[Γ ||-<lA> u ≅ v : A | RA]< wl > ->
+  W[Γ ||-<lA> t ≅ v : A | RA]< wl >.
+Proof.
+  intros [d Hd] [d' Hd'].
+  exists (DTree_fusion _ d d').
+  intros wl' Hover Hover' ; eapply transEqTerm.
+  - eapply Hd ; now eapply over_tree_fusion_l.
+  - eapply Hd' ; now eapply over_tree_fusion_r.
+Qed.  
 
 #[global]
 Instance perLRTmEq@{i j k l} {wl Γ l A} (RA : [LogRel@{i j k l} l | Γ ||- A]< wl >):
@@ -270,6 +290,15 @@ Proof.
   - intros ???; now eapply transEqTerm.
 Qed.
 
+#[global]
+Instance perWLRTmEq@{i j k l} {wl Γ l A} (RA : WLogRel@{i j k l} l wl Γ A):
+  Coq.Classes.CRelationClasses.PER@{Set k} (fun t u => W[ _ ||-< l > t ≅ u : _ | RA]< wl >).
+Proof.
+  econstructor.
+  - intros ???; now eapply WLRTmEqSym.
+  - intros ???; now eapply WtransEqTerm.
+Qed.
+
 Lemma LREqTermSymConv {wl Γ t u G G' l RG RG'} :
   [Γ ||-<l> t ≅ u : G | RG]< wl > -> 
   [Γ ||-<l> G' ≅ G | RG']< wl > ->
@@ -278,7 +307,17 @@ Proof.
   intros Rtu RGG'.
   eapply LRTmEqSym; eapply LRTmEqRedConv; tea.
   now eapply LRTyEqSym.
-Qed.  
+Qed.
+
+Lemma WLREqTermSymConv {wl Γ t u G G' l RG RG'} :
+  W[Γ ||-<l> t ≅ u : G | RG]< wl > -> 
+  W[Γ ||-<l> G' ≅ G | RG']< wl > ->
+  W[Γ ||-<l> u ≅ t : G' | RG']< wl >.
+Proof.
+  intros Rtu RGG'.
+  eapply WLRTmEqSym; eapply WLRTmEqRedConv; tea.
+  now eapply WLRTyEqSym.
+Qed.
 
 Lemma LREqTermHelper {wl Γ t t' u u' G G' l RG RG'} :
   [Γ ||-<l> t ≅ u : G | RG]< wl > -> 
@@ -290,7 +329,19 @@ Proof.
   intros Rtu Rtu' RGG' Ruu'.
   do 2  (eapply transEqTerm; tea).
   now eapply LREqTermSymConv.
-Qed.  
+Qed.
+
+Lemma WLREqTermHelper {wl Γ t t' u u' G G' l RG RG'} :
+  W[Γ ||-<l> t ≅ u : G | RG]< wl > -> 
+  W[Γ ||-<l> t' ≅ u' : G' | RG']< wl > -> 
+  W[Γ ||-<l> G ≅ G' | RG]< wl > ->
+  W[Γ ||-<l> u ≅ u' : G | RG]< wl > -> 
+  W[Γ ||-<l> t ≅ t' : G | RG]< wl >.
+Proof.
+  intros Rtu Rtu' RGG' Ruu'.
+  do 2  (eapply WtransEqTerm; tea).
+  now eapply WLREqTermSymConv.
+Qed. 
 
 End Transitivity.
 
diff --git a/theories/LogicalRelation/Weakening.v b/theories/LogicalRelation/Weakening.v
index a463c18..d62043c 100644
--- a/theories/LogicalRelation/Weakening.v
+++ b/theories/LogicalRelation/Weakening.v
@@ -538,687 +538,3 @@ Lemma wkEq@{i j k l} {wl Γ Δ A B l} (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]< wl >) (lr
   Qed.
 End Weakenings.
 
-
-Section Red_Ltrans.
-  Context `{GenericTypingProperties}.
-  
-Lemma Id_Ltrans@{h i j k l} (l : TypeLevel) (wl : wfLCon) (Γ : context) (A : term)
-  (IA : IdRedTy@{i j k l} wl Γ l A)
-  (ih1 : forall wl' : wfLCon,
-      wl' ≤ε wl -> [LogRel@{i j k l} l | Γ ||- IdRedTy.ty@{i j k l} IA ]< wl' >)
-  (ih2 : forall (Δ : context) (wl' : wfLCon) (ρ : Δ ≤ Γ),
-      wl' ≤ε wl -> [ |-[ ta ] Δ ]< wl' > ->
-      forall wl'' : wfLCon,
-        wl'' ≤ε wl' ->
-        [LogRel@{i j k l} l | Δ ||- (IdRedTy.ty@{i j k l} IA)⟨ρ⟩ ]< wl'' >)
-  (wl' : wfLCon)
-  (f : wl' ≤ε wl)
-  (Hg : [ |-[ ta ] Γ ]< wl >) : IdRedTy@{i j k l} wl' Γ l A.
-Proof.
-  unshelve econstructor.
-  6: econstructor ; [eapply wft_Ltrans, (IdRedTy.red IA).(tyr_wf_r _ _ _ _) ; eauto |
-                      eapply redty_Ltrans ; eauto].
-  3: now eapply (IdRedTy.red IA).(tyr_wf_red _ _ _ _).
-  3: eapply convty_Ltrans ; eauto ; now eapply (IdRedTy.eq IA).
-  + now eapply ih1.
-  + intros * f' Hd ; eapply ih2 ; [ | eassumption | now eapply wfLCon_le_id].
-    now eapply wfLCon_le_trans.
-  + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-    destruct (wk_id_ren_on Γ  (IdRedTy.lhs IA)). 
-    eapply (IdRedTy.tyKripkeTm IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
-    * now bsimpl.
-    * irrelevance0 ; [symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-      now eapply (IdRedTy.lhsRed).
-  + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-    destruct (wk_id_ren_on Γ  (IdRedTy.rhs IA)).
-    eapply (IdRedTy.tyKripkeTm IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
-    * now bsimpl.
-    * irrelevance0 ; [symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-      now eapply (IdRedTy.rhsRed).
-  + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-    destruct (wk_id_ren_on Γ  (IdRedTy.lhs IA)).
-    eapply (IdRedTy.tyKripkeTmEq IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
-    * now bsimpl.
-    * irrelevance0 ; [symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-      now eapply (IdRedTy.lhsRedRefl).
-  + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-    destruct (wk_id_ren_on Γ  (IdRedTy.rhs IA)).
-    eapply (IdRedTy.tyKripkeTmEq IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
-    * now bsimpl.
-    * irrelevance0 ; [symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-      now eapply (IdRedTy.rhsRedRefl).
-  + econstructor.
-    * intros ??? ; eapply (LREqTermSymConv); [eassumption | ].
-      now eapply reflLRTyEq.
-    * intros ????? ; eapply (transEqTerm@{h i j k l}) ; eassumption.
-  + intros ?? wl'' wl''' ??? f' f'' ??? Heq Hyp.
-    irrelevance0 ; [reflexivity | ].
-    eapply (IdRedTy.tyKripkeEq IA _ _ _ (f' •ε f) f'' wfΔ wfΞ _ Heq).
-    irrelevance0 ; [ reflexivity | eassumption].
-  + intros ?? wl'' wl''' ??? f' f'' ??? Heq Hyp.
-    irrelevance0 ; [reflexivity | ].
-    eapply (IdRedTy.tyKripkeTm IA _ _ _ (f' •ε f) f'' wfΔ wfΞ _ Heq).
-    irrelevance0 ; [ reflexivity | eassumption].
-  + intros ?? wl'' wl''' ??? f' f'' ???? Heq Hyp.
-    irrelevance0 ; [reflexivity | ].
-    eapply (IdRedTy.tyKripkeTmEq IA _ _ _ (f' •ε f) f'' wfΔ wfΞ _ _ Heq).
-    irrelevance0 ; [ reflexivity | eassumption].
-Defined.
-
-  Lemma Ltrans@{h i j k l} {wl Γ wl' A l} :
-    (wl' ≤ε wl) ->
-    [LogRel@{i j k l} l | Γ ||- A]< wl > ->
-    [LogRel@{i j k l} l | Γ ||- A]< wl' >.
-  Proof.
-    intros f lrA. revert wl' f. pattern l, wl, Γ, A, lrA.
-    eapply LR_rect_TyUr@{i j k l l}; clear l wl Γ A lrA.
-    - intros * [??? []] ??. apply LRU_.
-      econstructor ; eauto ; [now eapply wfc_Ltrans | econstructor ].
-      + now eapply wft_Ltrans.
-      + now eapply redty_Ltrans.
-    - intros ????[ty[]]??. apply LRne_ ; econstructor ; [econstructor | ].
-      + now eapply wft_Ltrans.
-      + now eapply redty_Ltrans.
-      + now eapply convneu_Ltrans.
-    - intros ???? [] ihdom ihcod wl' f ; cbn in *.
-      apply LRPi' ; econstructor ; [destruct red ; econstructor |..].
-      + now eapply wft_Ltrans.
-      + now eapply redty_Ltrans.
-      + now eapply convty_Ltrans.
-      + now eapply convty_Ltrans.
-      + unshelve econstructor.
-        4,5: destruct polyRed ; now eapply wft_Ltrans.
-        * intros * f' Hd.
-          eapply (PolyRed.shpRed polyRed) ; [eapply wfLCon_le_trans | ] ; eauto.
-        * intros ???? f' Hd ha ; cbn in *.
-          eapply (PolyRed.posTree polyRed) ; eauto.
-        * intros ???? f' ??? Hover ; cbn in *.
-          eapply (PolyRed.posRed polyRed) ; eassumption.
-        * intros ???? f' ????? Hover Hover' ; cbn in *.
-          eapply (PolyRed.posExt polyRed) ; eassumption.
-    - intros ????? wl' f.
-      eapply LRNat_ ; econstructor.
-      eapply redtywf_Ltrans ; eauto.
-      now eapply NA.(NatRedTy.red).
-    - intros ????? wl' f.
-      eapply LRBool_ ; econstructor.
-      eapply redtywf_Ltrans ; eauto.
-      now eapply NA.(BoolRedTy.red).
-    - intros ????? wl' f.
-      eapply LREmpty_ ; econstructor.
-      eapply redtywf_Ltrans ; eauto.
-      now eapply NA.(EmptyRedTy.red).
-    - intros ???? [] ihdom ihcod wl' f ; cbn in *.
-      apply (LRSig'@{i j k l}) ; econstructor ; [destruct red ; econstructor |..].
-      + now eapply wft_Ltrans.
-      + now eapply redty_Ltrans.
-      + now eapply convty_Ltrans.
-      + now eapply convty_Ltrans.
-      + unshelve econstructor.
-        4,5: destruct polyRed ; now eapply wft_Ltrans.
-        * intros * f' Hd.
-          eapply (PolyRed.shpRed polyRed) ; [eapply wfLCon_le_trans | ] ; eauto.
-        * intros ???? f' Hd ha ; cbn in *.
-          eapply (PolyRed.posTree polyRed) ; eauto.
-        * intros ???? f' ??? Hover ; cbn in *.
-          eapply (PolyRed.posRed polyRed) ; eassumption.
-        * intros ???? f' ????? Hover Hover' ; cbn in *.
-          eapply (PolyRed.posExt polyRed) ; eassumption.
-    - intros ????? ih1 ih2 wl' f. 
-      apply (LRId'@{i j k l}).
-      eapply (Id_Ltrans@{h i j k l}) ; eauto.
-      now eapply (wfc_convty (IdRedTy.eq IA)).
-  Defined.
-
-  
-Lemma Eq_Ltrans@{h i j k l} {wl Γ wl' A B l} (f : wl' ≤ε wl) (lrA : [Γ ||-<l> A]< wl >) : 
-    [LogRel@{i j k l} l | Γ ||- A ≅ B | lrA]< wl > ->
-    [LogRel@{i j k l} l | Γ ||- A ≅ B | Ltrans@{h i j k l} f lrA]< wl' >.
-Proof.
-  revert B wl' f. pattern l, wl, Γ, A, lrA.
-  eapply LR_rect_TyUr@{i j k l l}; clear l wl Γ A lrA.
-  - intros ???? [??? []] ???[] ; cbn in *.
-    constructor ; constructor.
-    + now eapply wft_Ltrans.
-    + destruct red ; now eapply redty_Ltrans.
-  - intros ???? [?[]] ???[?[]] ; cbn in *.
-    econstructor ; [econstructor | ].
-    + now eapply wft_Ltrans.
-    + now eapply redty_Ltrans.
-    + now eapply convneu_Ltrans.
-  - intros ???? [] ihdom ihcod B wl' f []; cbn in *.
-    econstructor ; [destruct red0 ; econstructor |..].
-    + now eapply wft_Ltrans.
-    + now eapply redty_Ltrans.
-    + now eapply convty_Ltrans.
-    + now eapply convty_Ltrans.
-    + unshelve econstructor ; cbn in *.
-      * intros * ? ; now eapply (PolyRedEq.posTree polyRed0).
-      * intros * ; now eapply (PolyRedEq.shpRed polyRed0).
-      * cbn ; intros * Ho' ; now eapply (PolyRedEq.posRed polyRed0).
-  - intros ???? [[]] B wl' f [[]] ; cbn in *.
-    econstructor ; econstructor.
-    + now eapply wft_Ltrans.
-    + now eapply redty_Ltrans.
-  - intros ???? [[]] B wl' f [[]] ; cbn in *.
-    econstructor ; econstructor.
-    + now eapply wft_Ltrans.
-    + now eapply redty_Ltrans.
-  - intros ???? [[]] B wl' f [[]] ; cbn in *.
-    econstructor ; econstructor.
-    + now eapply wft_Ltrans.
-    + now eapply redty_Ltrans.
-  - intros ???? [] ihdom ihcod B wl' f [] ; cbn in *.
-    econstructor ; [destruct red0 ; econstructor | ..].
-    + now eapply wft_Ltrans.
-    + now eapply redty_Ltrans.
-    + now eapply convty_Ltrans.
-    + now eapply convty_Ltrans.
-    + unshelve econstructor ; cbn.
-      * intros * ? ; now eapply (PolyRedEq.posTree polyRed0).
-      * intros * ; now eapply (PolyRedEq.shpRed polyRed0).
-      * cbn ; intros * Ho' ; now eapply (PolyRedEq.posRed polyRed0).
-  - intros ????? ih1 ih2 ????.
-    assert (Hg:= (wfc_convty (IdRedTy.eq IA))).
-    eapply (@Build_IdRedTyEq _ _ _ _ _ _ wl' Γ A _ B) ; cbn.
-    + unshelve econstructor.
-      * now eapply wft_Ltrans, (IdRedTyEq.red X).(tyr_wf_r _ _ _ _).
-      * now eapply redty_Ltrans, (IdRedTyEq.red X).(tyr_wf_red _ _ _ _).
-    + eapply convty_Ltrans ; [ eassumption | ].
-      eapply (IdRedTyEq.eq X). 
-    + eapply ih1.
-      now eapply (IdRedTyEq.tyRed X).
-    + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-      destruct (wk_id_ren_on Γ  (IdRedTy.lhs IA)).
-      destruct (wk_id_ren_on Γ  (IdRedTyEq.lhs X)).
-      eapply (IdRedTy.tyKripkeTmEq IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
-      * now bsimpl.
-      * irrelevance0 ; [ symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-        exact (IdRedTyEq.lhsRed X).
-    + irrelevance0 ; [ now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-      destruct (wk_id_ren_on Γ  (IdRedTy.rhs IA)).
-      destruct (wk_id_ren_on Γ  (IdRedTyEq.rhs X)).
-      eapply (IdRedTy.tyKripkeTmEq IA wk_id _ _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
-      * now bsimpl.
-      * irrelevance0 ; [ symmetry ; now eapply (wk_id_ren_on Γ (IdRedTy.ty IA)) | ].
-        exact (IdRedTyEq.rhsRed X).
-Qed.
-
-
-Lemma isLRFun_Ltrans : forall wl wl' Γ t A l (f : wl' ≤ε wl) (ΠA : [Γ ||-Π< l > A]< wl >)
-                              (ΠA' : [Γ ||-Π< l > A]< wl' >),
-    isLRFun ΠA t -> isLRFun ΠA' t.
-Proof.
-  intros * f * Hyp.
-  unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)).
-  1,2: now econstructor.
-  inversion Heq.
-  induction Hyp as [?? funTree e r | t Heqt].
-  - unshelve econstructor.
-    + intros Δ wl'' a ρ f' Hd ha ; cbn.
-      eapply DTree_fusion.
-      * unshelve eapply funTree.
-        6: irrelevance0 ; [ | exact ha] ; now f_equal.
-        2: assumption.
-        now eapply wfLCon_le_trans.
-      * unshelve eapply (PolyRedPack.posTree ΠA).
-        5: eassumption.
-        4: irrelevance0 ; [ | exact ha] ; now f_equal.
-        now eapply wfLCon_le_trans.
-    + intros Δ wl'' ρ f' Hd ; cbn.
-      irrelevance0 ; [ | unshelve eapply e] ; [now f_equal | ..].
-      2: assumption.
-      now eapply wfLCon_le_trans.
-    + intros Δ wl'' a ρ f' Hd ha wl''' Ho Ho'.
-      irrelevance0 ; [ | unshelve eapply r].
-      now f_equal.
-      3: eassumption.
-      now eapply wfLCon_le_trans.
-      cbn in *.
-      3: now eapply over_tree_fusion_l.
-      now eapply over_tree_fusion_r.
-  - econstructor 2.
-    cbn in *.
-    rewrite <- H11, <- H12.
-    now eapply convneu_Ltrans.
-Qed.
-
-Lemma isLRPair_Ltrans : forall wl wl' Γ t A l (f : wl' ≤ε wl) (ΣA : [Γ ||-Σ< l > A]< wl >)
-                              (ΣA' : [Γ ||-Σ< l > A]< wl' >),
-    isLRPair ΣA t -> isLRPair ΣA' t.
-Proof.
-  intros * f * Hyp.
-  unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΣA.(ParamRedTyPack.red)) ΣA'.(ParamRedTyPack.red)).
-  1,2: now econstructor.
-  inversion Heq.
-  induction Hyp as [????? fstTree ?? sndTree | t Heqt].
-  - unshelve econstructor.
-    + intros Δ wl'' a' ρ f' Hd ha ; cbn.
-      eapply DTree_fusion.
-      * unshelve eapply fstTree.
-        6: irrelevance0 ; [ | exact ha] ; now f_equal.
-        2: assumption.
-        now eapply wfLCon_le_trans.
-      * unshelve eapply (PolyRedPack.posTree ΣA).
-        5: eassumption.
-        4: irrelevance0 ; [ | exact ha] ; now f_equal.
-        now eapply wfLCon_le_trans.
-    + intros Δ wl'' ρ f' Hd ; cbn.
-      irrelevance0 ; [ | unshelve eapply rfst] ; [now f_equal | ..].
-      2: assumption.
-      now eapply wfLCon_le_trans.
-    + intros Δ wl'' ρ f' Hd.
-      eapply DTree_fusion.
-      * eapply sndTree.
-        1,3: eassumption.
-        now eapply wfLCon_le_trans.
-      * unshelve  eapply (PolyRed.posTree ΣA).
-        6: now unshelve eapply rfst.
-        2,4: eassumption.
-        now eapply wfLCon_le_trans.
-    + intros Δ wl'' ρ f' Hd.
-      irrelevance0 ; [ | unshelve eapply rdom ; eauto].
-      now f_equal.
-      now eapply wfLCon_le_trans.
-    + intros Δ wl'' a' ρ f' Hd ha wl''' Ho Ho' ; cbn in *.
-      irrelevance0 ; [ | unshelve eapply rcod].
-      1: now f_equal.
-      3: eassumption.
-      * now eapply wfLCon_le_trans.
-      * irrelevance0 ; [ | exact ha] ; now f_equal.
-      * cbn in * ; now eapply over_tree_fusion_r.
-      * cbn in * ; now eapply over_tree_fusion_l.
-    + intros Δ wl'' ρ f' Hd wl''' Ho Ho' ; cbn in *.
-      irrelevance0 ; [ | unshelve eapply rsnd].
-      1: now f_equal.
-      3: eassumption.
-      * now eapply wfLCon_le_trans.
-      * cbn in * ; now eapply over_tree_fusion_r.
-      * cbn in * ; now eapply over_tree_fusion_l.
-  - econstructor 2.
-    cbn in *.
-    rewrite <- H11, <- H12.
-    now eapply convneu_Ltrans.
-Qed.
-
-Lemma NatTm_Ltrans (l : TypeLevel) (wl : wfLCon) (Γ : context) (A : term)
-  (NA : [Γ ||-Nat A ]< wl >) (t : term) (wl' : wfLCon) (f : wl' ≤ε wl) (NA' : [Γ ||-Nat A ]< wl' >) :
-  [LRNat_ l NA | Γ ||- t : A ]< wl > -> [ (LRNat_ l NA') | Γ ||- t : A ]< wl' >.
-Proof.
-  revert t.
-  set (G := _); enough (h : G × (forall t, NatProp NA t -> NatProp NA' t)) by apply h.
-  subst G; apply NatRedInduction.
-  - intros t nf Hred Heq Hprop Hprop'.
-    econstructor ; [now eapply redtmwf_Ltrans | | ].
-    + now eapply convtm_Ltrans.
-    + assumption.
-  - now econstructor.
-  - intros n Hn Hn' ; now econstructor.
-  - intros ; econstructor.
-    destruct r ; econstructor.
-    + now eapply ty_Ltrans.
-    + now eapply convneu_Ltrans.
-Qed.
-
-Lemma IdTm_Ltrans (l : TypeLevel) (wl wl' : wfLCon) (Γ : context) (A : term) (f : wl' ≤ε wl)
-  (IA : [Γ ||-Id< l > A ]< wl >) (IA' : [Γ ||-Id< l > A ]< wl' >)
-  (ih1 : forall (t : term),
-      [IdRedTy.tyRed IA | Γ ||- t : IdRedTy.ty IA ]< wl > ->
-      [IdRedTy.tyRed IA' | Γ ||- t : IdRedTy.ty IA' ]< wl' >)
-  (ih2 : forall (Δ : context) (ρ : Δ ≤ Γ) (wfΔ : [ |-[ ta ] Δ ]< wl' >)
-                (t : term) (wl'' : wfLCon) (f' : wl'' ≤ε wl'),
-      [IdRedTy.tyKripke IA ρ f wfΔ | Δ ||- t : (IdRedTy.ty IA)⟨ρ⟩ ]< wl' > ->
-      [IdRedTy.tyKripke IA' ρ f' (wfc_Ltrans f' wfΔ) | Δ ||- t : (IdRedTy.ty IA')⟨ρ⟩ ]< wl'' >) :
-      forall (t : term),
-        [LRId' IA | Γ ||- t : A ]< wl > -> [LRId' IA' | Γ ||- t : A ]< wl' >.
-Proof.
-  intros t Ht.
-  unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f (IdRedTy.red IA))
-                           (IdRedTy.red IA')).
-  1,2 : now econstructor.
-  inversion Heq.
-  assert (Hg:= (wfc_convty (IdRedTy.eq IA))).
-  econstructor ; cbn.
-  - cbv in H11,H12,H13 ; cbv. 
-    rewrite <- H11, <- H12, <- H13.
-    now eapply redtmwf_Ltrans ; [ | eapply (IdRedTm.red Ht)].
-  - cbv in H11,H12,H13 ; cbv. 
-    rewrite <- H11, <- H12, <- H13.
-    now eapply convtm_Ltrans ; [ | eapply (IdRedTm.eq Ht)].
-  - destruct (IdRedTm.prop Ht).
-    + econstructor.
-      * now eapply wft_Ltrans.
-      * now eapply ty_Ltrans.
-      * irrelevance0 ; [ | unshelve eapply Eq_Ltrans].
-        5: eassumption.
-        all: assumption.
-      * assert (Help : IdRedTyPack.lhs (IdRedTy.toPack IA') = IdRedTyPack.lhs (IdRedTy.toPack IA)).
-        { now eauto. }
-        rewrite Help.
-        irrelevance0.
-        2:{ erewrite <- (wk_id_ren_on Γ (IdRedTyPack.lhs (IdRedTy.toPack IA))).
-            erewrite <- wk_id_ren_on.
-            eapply (IdRedTy.tyKripkeTmEq IA wk_id wk_id _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
-            * now bsimpl.
-            * irrelevance0 ; [rewrite wk_id_ren_on ; reflexivity | ].
-              eassumption.
-        }
-        rewrite H11 ; bsimpl.
-        reflexivity.
-      * assert (Help : IdRedTyPack.rhs (IdRedTy.toPack IA') = IdRedTyPack.rhs (IdRedTy.toPack IA)).
-        { now eauto. }
-        rewrite Help.
-        irrelevance0.
-        2:{ erewrite <- (wk_id_ren_on Γ (IdRedTyPack.rhs (IdRedTy.toPack IA))).
-            erewrite <- wk_id_ren_on.
-            eapply (IdRedTy.tyKripkeTmEq IA wk_id wk_id _ (wfLCon_le_id _) f Hg (wfc_Ltrans f Hg)).
-            * now bsimpl.
-            * irrelevance0 ; [rewrite wk_id_ren_on ; reflexivity | ].
-              eassumption.
-        }
-        rewrite H11 ; bsimpl.
-        reflexivity.
-    + econstructor.
-      destruct r ; econstructor.
-      * eapply ty_Ltrans ; [eassumption | ].
-        assert (Help : IdRedTyPack.outTy (IdRedTy.toPack IA') = IdRedTyPack.outTy (IdRedTy.toPack IA)) by eauto.
-        now rewrite Help.
-      * eapply convneu_Ltrans ; [eassumption | ].
-        assert (Help : IdRedTyPack.outTy (IdRedTy.toPack IA') = IdRedTyPack.outTy (IdRedTy.toPack IA)) by eauto.
-        now rewrite Help.
-Qed.
-
-Lemma ΠTm_Ltrans (l : TypeLevel) (wl wl' : wfLCon) (Γ : context) (f : wl' ≤ε wl) (A : term)
-  (ΠA : [Γ ||-Π< l > A ]< wl >)
-  (ΠA' : [Γ ||-Π< l > A ]< wl' >)
-  (ihdom : forall (Δ : context) (ρ : Δ ≤ Γ) (h : [ |-[ ta ] Δ ]< wl' >) (t : term)
-                  (wl'' : wfLCon) (f' : wl'' ≤ε wl'),
-      [PolyRed.shpRed ΠA ρ f h | Δ ||- t : (ParamRedTy.dom ΠA)⟨ρ⟩ ]< wl' > ->
-      [Ltrans f' (PolyRed.shpRed ΠA ρ f h) | Δ ||- t : (ParamRedTy.dom ΠA)⟨ρ⟩ ]< wl'' >)
-  (ihcod : forall (Δ : context) (a : term) (ρ : Δ ≤ Γ) (h : [ |-[ ta ] Δ ]< wl' >)
-                  (ha : [PolyRed.shpRed ΠA ρ f h | Δ ||- a : (ParamRedTy.dom ΠA)⟨ρ⟩ ]< wl' >)
-                  (wl'' : wfLCon) (Ho : over_tree wl' wl'' (PolyRed.posTree ΠA ρ f h ha))
-                  (t : term) (wl''' : wfLCon) (f'' : wl''' ≤ε wl''),
-      [PolyRed.posRed ΠA ρ f h ha Ho | Δ  ||- t : (ParamRedTy.cod ΠA)[a .: ρ >> tRel] ]< wl'' > ->
-      [Ltrans f'' (PolyRed.posRed ΠA ρ f h ha Ho) | Δ  ||- t : (ParamRedTy.cod ΠA)[a .: ρ >> tRel] ]< wl''' >) :
-  forall (t : term),
-    [Γ ||-Π t : A | ΠA ]< wl > ->  [Γ ||-Π t : A | ΠA' ]< wl' >.
-Proof.
-  intros t [].
-  unshelve econstructor ; [ | | eapply redtmwf_Ltrans ; eauto |..].
-  1: exact nf.
-  1:{ cbn in * ; intros.
-      eapply DTree_fusion.
-      * unshelve eapply appTree.
-        4: eapply wfLCon_le_trans.
-        3-6: eassumption.
-        2: irrelevance0 ; [ | eassumption ].
-        f_equal.
-        unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)) ; [now econstructor | now econstructor | ].
-        now inversion Heq.
-    * eapply (PolyRed.posTree ΠA ρ (f0 •ε f) Hd).
-      irrelevance0 ; [ | eassumption].
-      f_equal.
-      unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)) ; [now econstructor | now econstructor | ].
-      now inversion Heq.
-  }
-  all: unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)) ; [now econstructor | now econstructor | ].
-  all: inversion Heq.
-  2: eapply convtm_Ltrans ; [eauto | now rewrite <- Heq].
-  2: eapply isLRFun_Ltrans ; eauto.
-  1: now rewrite <- Heq.
-  + cbn in * ; intros. 
-    irrelevance0 ; [ | unshelve eapply app].
-    6: now eapply over_tree_fusion_r.
-    * now f_equal.
-    * now eapply over_tree_fusion_l.
-  + cbn in * ; intros.
-    irrelevance0 ; [ | unshelve eapply eq].
-    9: now eapply over_tree_fusion_l.
-    2: now eapply over_tree_fusion_r.
-    1: now f_equal.
-    1,2: irrelevance0 ; [ | eassumption] ; now f_equal.
-Defined.
-
-Lemma ΣTm_Ltrans (l : TypeLevel) (wl wl' : wfLCon) (Γ : context) (f : wl' ≤ε wl) (A : term)
-  (ΣA : [Γ ||-Σ< l > A ]< wl >)
-  (ΣA' : [Γ ||-Σ< l > A ]< wl' >)
-  (ihdom : forall (Δ : context) (ρ : Δ ≤ Γ) (h : [ |-[ ta ] Δ ]< wl' >) (t : term)
-                  (wl'' : wfLCon) (f' : wl'' ≤ε wl'),
-      [PolyRed.shpRed ΣA ρ f h | Δ ||- t : (ParamRedTy.dom ΣA)⟨ρ⟩ ]< wl' > ->
-      [Ltrans f' (PolyRed.shpRed ΣA ρ f h) | Δ ||- t : (ParamRedTy.dom ΣA)⟨ρ⟩ ]< wl'' >)
-  (ihcod : forall (Δ : context) (a : term) (ρ : Δ ≤ Γ) (h : [ |-[ ta ] Δ ]< wl' >)
-                  (ha : [PolyRed.shpRed ΣA ρ f h | Δ ||- a : (ParamRedTy.dom ΣA)⟨ρ⟩ ]< wl' >)
-                  (wl'' : wfLCon) (Ho : over_tree wl' wl'' (PolyRed.posTree ΣA ρ f h ha))
-                  (t : term) (wl''' : wfLCon) (f'' : wl''' ≤ε wl''),
-      [PolyRed.posRed ΣA ρ f h ha Ho | Δ  ||- t : (ParamRedTy.cod ΣA)[a .: ρ >> tRel] ]< wl'' > ->
-      [Ltrans f'' (PolyRed.posRed ΣA ρ f h ha Ho) | Δ  ||- t : (ParamRedTy.cod ΣA)[a .: ρ >> tRel] ]< wl''' >) :
-  forall (t : term),
-    [Γ ||-Σ t : A | ΣA ]< wl > ->  [Γ ||-Σ t : A | ΣA' ]< wl' >.
-Proof.
-  intros t [].
-  unshelve econstructor.
-  4: eapply redtmwf_Ltrans ; eauto.
-  1: exact nf.
-  2:{ cbn in * ; intros.
-      eapply DTree_fusion.
-      * unshelve eapply sndTree.
-        3: eapply wfLCon_le_trans.
-        2-5: eassumption.
-      * eapply (PolyRed.posTree ΣA ρ (f0 •ε f) Hd).
-        eapply fstRed.
-  }
-  all: unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΣA.(ParamRedTyPack.red)) ΣA'.(ParamRedTyPack.red)) ; [now econstructor | now econstructor | ].
-  all: inversion Heq.
-  3: eapply convtm_Ltrans ; [eauto | ].
-  2,3: cbv ; cbv in Heq ; now rewrite <- Heq.
-  2: eapply isLRPair_Ltrans ; now eauto.
-  + cbn in * ; intros.
-    irrelevance0 ; [ | unshelve eapply fstRed].
-    * now f_equal.
-    * now eapply wfLCon_le_trans.
-    * assumption.
-  + cbn in * ; intros.
-    irrelevance0 ; [ | unshelve eapply sndRed].
-    4: eassumption.
-    * now f_equal.
-    * now eapply wfLCon_le_trans.
-    * now eapply over_tree_fusion_r.
-    * now eapply over_tree_fusion_l.
-Defined.
-  
-Lemma Tm_Ltrans@{h i j k l} {wl Γ wl' t A l} (f : wl' ≤ε wl) (lrA : [Γ ||-<l> A]< wl >) : 
-    [LogRel@{i j k l} l | Γ ||- t : A | lrA]< wl > ->
-    [LogRel@{i j k l} l | Γ ||- t : A | Ltrans@{h i j k l} f lrA]< wl' >.
-Proof.
-  revert t wl' f. pattern l, wl, Γ, A, lrA.
-  eapply LR_rect_TyUr@{i j k l l}; clear l wl Γ A lrA.
-  - intros ???? [??? []] ???[?[]].
-    econstructor ; [ econstructor | eassumption |.. ].
-    + now eapply ty_Ltrans.
-    + now eapply redtm_Ltrans.
-    + now eapply convtm_Ltrans.
-    + apply RedTyRecBwd ; apply RedTyRecFwd in rel.
-      now eapply Ltrans ; eauto.
-  - intros ???? [?[]] ???[?[]] ; cbn in *.
-    econstructor ; [econstructor ; cbn | ].
-    + now eapply ty_Ltrans.
-    + now eapply redtm_Ltrans.
-    + now eapply convneu_Ltrans.
-  - intros ???? [] ihdom ihcod t wl' f ?.
-    cbn in *.
-    unshelve eapply ΠTm_Ltrans ; intros.
-    6: eassumption.
-    1: eassumption.
-    + now eapply ihdom.
-    + now eapply ihcod. 
-  - intros ; irrelevance0 ; [ reflexivity | unshelve eapply NatTm_Ltrans].
-    5: eassumption.
-    2: assumption.
-    destruct NA ; econstructor ; now eapply redtywf_Ltrans.
-  - intros ???? NA t ? f ; revert t ; cbn.
-    intros t Ht. induction Ht. econstructor.
-    + now eapply redtmwf_Ltrans.
-    + now eapply convtm_Ltrans.
-    + destruct prop as [ | | m Hne] ; econstructor.
-      destruct Hne ; econstructor.
-      * now eapply ty_Ltrans.
-      * now eapply convneu_Ltrans.
-  - intros ???? NA t ? f Ht ; cbn.
-    induction Ht ; econstructor.
-    + now eapply redtmwf_Ltrans.
-    + now eapply convtm_Ltrans.
-    + destruct prop as [m Hne] ; econstructor.
-      destruct Hne ; econstructor.
-      * now eapply ty_Ltrans.
-      * now eapply convneu_Ltrans.
-  - intros ????? ihdom ihcod t wl' f ?; cbn in *.
-    eapply ΣTm_Ltrans.
-    + intros ; eauto.
-    + intros ; eauto.
-    + assumption.
-      Unshelve. assumption.
-  - intros * ih1 ih2 *.
-    unshelve eapply IdTm_Ltrans.
-    eassumption.
-    + intros ; eapply ih1 ; auto.
-    + intros ; eapply ih2.
-      rewrite <- (wk_id_ren_on Δ t0).
-      eapply (IdRedTy.tyKripkeTm IA ρ).
-      * now bsimpl.
-      * eassumption.
-Qed.
-
-Lemma TmEq_Ltrans@{h i j k l} {wl Γ wl' t u A l} (f : wl' ≤ε wl) (lrA : [Γ ||-<l> A]< wl >) : 
-    [LogRel@{i j k l} l | Γ ||- t ≅ u : A | lrA]< wl > ->
-    [LogRel@{i j k l} l | Γ ||- t ≅ u : A | Ltrans@{h i j k l} f lrA]< wl' >.
-Proof.
-  revert t u wl' f. pattern l, wl, Γ, A, lrA.
-  eapply LR_rect_TyUr@{i j k l l}; clear l wl Γ A lrA.
-  - intros ???? [??? []] ???? [].
-    unshelve econstructor.
-    + destruct redL.
-      econstructor.
-      * now eapply redtmwf_Ltrans.
-      * assumption.
-      * now eapply convtm_Ltrans.
-      * apply RedTyRecBwd ; clear relEq ; apply RedTyRecFwd in relL.
-        now eapply Ltrans.
-    + destruct redR.
-      econstructor.
-      * now eapply redtmwf_Ltrans.
-      * assumption.
-      * now eapply convtm_Ltrans.
-      * apply RedTyRecBwd ; clear relEq ; apply RedTyRecFwd in relR.
-        now eapply Ltrans.
-    + apply RedTyRecBwd ; clear relEq ; apply RedTyRecFwd in relL.
-      now eapply Ltrans.
-    + cbn in *.
-      now eapply convtm_Ltrans.
-    + apply RedTyRecBwd ; clear relEq ; apply RedTyRecFwd in relR.
-      now eapply Ltrans.
-    + eapply TyEqRecBwd, Eq_Ltrans ; cbn.
-      now eapply TyEqRecFwd.
-  - intros ???? [?[]] ???? [] ; cbn in *.
-    econstructor.
-    + now eapply redtmwf_Ltrans.
-    + now eapply redtmwf_Ltrans.
-    + now eapply convneu_Ltrans.
-  - intros ????? ihdom ihcod t u wl' f [].
-    cbn.
-    unshelve econstructor ; cbn in *.
-    + unshelve eapply ΠTm_Ltrans ; [ | eassumption | ..].
-      1,4: eassumption.
-      * intros ; now eapply Tm_Ltrans.
-      * intros ; now eapply Tm_Ltrans.
-    + unshelve eapply ΠTm_Ltrans ; [ | eassumption | ..].
-      1,4: eassumption.
-      * intros ; now eapply Tm_Ltrans.
-      * intros ; now eapply Tm_Ltrans.
-    + intros ; eapply eqTree.
-      eassumption.
-    + intros ; cbn in *.
-      now eapply convtm_Ltrans.
-    + intros ; cbn in *.
-      eapply eqApp.
-      assumption.
-  - intros * ; revert t u.
-    set (NA' := {| NatRedTy.red := redtywf_Ltrans f (NatRedTy.red NA) |}).
-    set (G := _); enough (h : G × (forall t u, NatPropEq NA t u -> NatPropEq NA' t u)) by apply h.
-    subst G; apply NatRedEqInduction.
-    + intros t u nt nu Hredt Hredu Heq Hprop Hprop'.
-      econstructor.
-      1,2: now eapply redtmwf_Ltrans.
-      * now eapply convtm_Ltrans.
-      * assumption.
-    + now econstructor.
-    + intros n Hn Hn' ; now econstructor.
-    + intros ; econstructor.
-      destruct r ; econstructor.
-      now eapply convneu_Ltrans.
-  - intros ???? NA t ? wl' f Heq.
-    induction Heq ; cbn. econstructor.
-    1,2: now eapply redtmwf_Ltrans.
-    + now eapply convtm_Ltrans.
-    + destruct prop as [ | | m Hne] ; econstructor.
-      econstructor.
-      now destruct r ; eapply convneu_Ltrans.
-  - intros ???? NA t u wl' f Heq ; cbn.
-    induction Heq ; econstructor.
-    1,2: now eapply redtmwf_Ltrans.
-    + now eapply convtm_Ltrans.
-    + destruct prop as [m Hne] ; econstructor ; econstructor.
-      now destruct r ; eapply convneu_Ltrans.
-  - cbn ; intros ????? ihdom ihcod t u wl' f []; cbn in *.
-    unshelve econstructor ; cbn.
-    + unshelve eapply ΣTm_Ltrans.
-      2,3,6: eassumption.
-      * intros.
-        irrelevance0 ; [ | unshelve eapply Tm_Ltrans].
-        5: eassumption.
-        1,2: now auto.
-      * intros.
-        irrelevance0 ; [ | unshelve eapply Tm_Ltrans].
-        5: eassumption.
-        1,2: now trivial.
-    + unshelve eapply ΣTm_Ltrans.
-      2,3,6: eassumption.
-      * intros.
-        irrelevance0 ; [ | unshelve eapply Tm_Ltrans].
-        5: eassumption.
-        1,2: now auto.
-      * intros.
-        irrelevance0 ; [ | unshelve eapply Tm_Ltrans].
-        5: eassumption.
-        1,2: now trivial.
-    + intros ; eapply DTree_fusion.
-      * eapply eqTree.
-        1,3: eassumption.
-        now eapply wfLCon_le_trans.
-      * eapply (PolyRed.posTree ΠA ρ (f0 •ε f) Hd).
-        now eapply (SigRedTm.fstRed redL). 
-    + cbn ; now eapply convtm_Ltrans.
-    + cbn ; intros ; now unshelve eapply eqFst.
-    + cbn in * ; intros.
-      irrelevance0 ; [ reflexivity | unshelve eapply eqSnd].
-      3: eassumption.
-      * now eapply wfLCon_le_trans.
-      * now eapply over_tree_fusion_r.
-      * now eapply over_tree_fusion_l.
-  - intros ????? ih1 ih2 ???? [].
-    unshelve econstructor ; cbn.
-    3,4: now eapply redtmwf_Ltrans.
-    1: now eapply convtm_Ltrans.
-    destruct prop.
-    + econstructor.
-      1,2: now eapply wft_Ltrans.
-      1,2: now eapply ty_Ltrans.
-      1,2:irrelevance0 ; [ | now eapply Eq_Ltrans] ; reflexivity.
-      all: now eapply ih1.
-    + econstructor.
-      destruct r ; econstructor.
-      now eapply convneu_Ltrans.
-      Unshelve. all: assumption.
-Qed.
-  
-End Red_Ltrans.
diff --git a/theories/Monad.v b/theories/Monad.v
index fba3f50..89165e2 100644
--- a/theories/Monad.v
+++ b/theories/Monad.v
@@ -197,7 +197,20 @@ Proof.
   - now inversion H.
 Qed.
 
-Lemma over_tree_LTrans (k k' k'' : wfLCon) (f : k' ≤ε k) (d : DTree k) :
+Lemma le_over_tree {k k' k'' d} : k'' ≤ε k' -> over_tree k k' d -> over_tree k k'' d.
+Proof.
+  induction d as [ | k n ne kt IHt kf IHf] ; cbn ; intros Hinf Hinf' ; auto.
+  - now eapply wfLCon_le_trans.
+  - destruct (decidInLCon k' n).
+    + erewrite (decidInLCon_true (Hinf _ _ i)).
+      now eapply IHt.
+    + erewrite (decidInLCon_false (Hinf _ _ i)).
+      now eapply IHf.
+    + now inversion Hinf'.
+Qed.
+  
+
+Lemma over_tree_Ltrans (k k' k'' : wfLCon) (f : k' ≤ε k) (d : DTree k) :
   over_tree k' k'' (DTree_Ltrans k k' f d) -> over_tree k k'' d.
 Proof.
   intros Hyp ; assert (f' : k'' ≤ε k') by now eapply over_tree_le.
@@ -224,6 +237,23 @@ Proof.
       * assumption.
 Qed.
 
+Lemma Ltrans_over_tree (k k' k'' : wfLCon) (f : k' ≤ε k) (f' : k'' ≤ε k') (d : DTree k) :
+  over_tree k k'' d -> over_tree k' k'' (DTree_Ltrans k k' f d).
+Proof.
+  revert k' k'' f f' ; induction d as [  | k n ne kt IHt kf IHf] ; intros * f' ; cbn.
+  - now eauto.
+  - destruct (decidInLCon k' n).
+    + rewrite (decidInLCon_true (f' n _ i)) ; intros H.
+      now eapply IHt.
+    + rewrite (decidInLCon_false (f' n _ i)) ; intros H.
+      now eapply IHf.
+    + cbn in *.
+      destruct (decidInLCon k'' n) ; cbn ; intros H ; eauto.
+      * eapply IHt ; eauto.
+        now eapply LCon_le_in_LCon ; eauto.
+      * eapply IHf ; eauto.
+        now eapply LCon_le_in_LCon ; eauto.
+Qed.
       
 Lemma over_tree_fusion_l k k' d d' :
   over_tree k k' (DTree_fusion k d d') ->
@@ -247,17 +277,18 @@ Proof.
   - eassumption.
   - cbn in * ; subst.
     destruct (decidInLCon k' n).
-    + eapply over_tree_LTrans, IHt ; eassumption.
-    + eapply over_tree_LTrans, IHf ; eassumption.
+    + eapply over_tree_Ltrans, IHt ; eassumption.
+    + eapply over_tree_Ltrans, IHf ; eassumption.
     + now inversion Hov.
 Qed.
 
 Arguments over_tree_fusion_l [_ _ _ _] _.
 Arguments over_tree_fusion_r [_ _ _ _] _.
 
-Lemma split_to_over_tree (wl : wfLCon)
+Lemma split_to_over_tree 
   (P : wfLCon -> Type)
   (Pe : forall wl n (ne : not_in_LCon (pi1 wl) n), P (wl ,,l (ne, true)) -> P (wl ,,l (ne, false)) -> P wl)
+  (wl : wfLCon)
   (d : DTree wl)
   (H : forall wl', over_tree wl wl' d -> P wl') : P wl. 
 Proof.
@@ -277,6 +308,66 @@ Proof.
       apply (over_tree_le Hover) ; now constructor.
 Qed.
 
+Lemma dsplit_to_over_tree (wl : wfLCon)
+  (P : forall wl', wl' ≤ε wl -> Type)
+  (Pe : forall wl' n (ne : not_in_LCon (pi1 wl') n) f ft ff,
+      P (wl' ,,l (ne, true)) ft -> P (wl' ,,l (ne, false)) ff -> P wl' f)
+  (d : DTree wl)
+  (H : forall wl' f, over_tree wl wl' d -> P wl' f) : P wl (idε _). 
+Proof.
+  enough (Hyp : forall wl' f, P wl' f) by apply Hyp.
+  revert P Pe H.
+  induction d ; intros P Pe H wl' f.
+  - now apply H.
+  - cbn in * ; destruct (decidInLCon wl' n).
+    + pose proof (Hinf := LCon_le_step (l := k) (b := true) ne (wfLCon_le_id _)).
+      specialize (IHd1 (fun wl' f => P wl' (wfLCon_le_trans f Hinf))).
+      cbn in *.
+      assert (Hinf' : wl' ≤ε (k,,l (ne, true))).
+      { now eapply LCon_le_in_LCon. }
+      change (P wl' (Hinf' •ε Hinf)).
+      eapply IHd1.
+      * intros ; eauto.
+      * intros wl'' f' Hover.
+        apply H ; cbn.
+        unshelve erewrite (decidInLCon_true _) ; [ | assumption].
+        now eapply f'; econstructor.
+    + pose proof (Hinf := LCon_le_step (l := k) (b := false) ne (wfLCon_le_id _)).
+      specialize (IHd2 (fun wl' f => P wl' (wfLCon_le_trans f Hinf))).
+      cbn in *.
+      assert (Hinf' : wl' ≤ε (k,,l (ne, false))).
+      { now eapply LCon_le_in_LCon. }
+      change (P wl' (Hinf' •ε Hinf)).
+      eapply IHd2.
+      * intros ; eauto.
+      * intros wl'' f' Hover.
+        apply H ; cbn.
+        unshelve erewrite (decidInLCon_false _) ; [ | assumption].
+        now eapply f'; econstructor.
+    + unshelve eapply (Pe _ _ n0).
+      1,2: now eapply wfLCon_le_trans ; [ eapply LCon_le_step | eapply (idε _)].
+      * pose proof (Hinf := LCon_le_step (l := k) (b := true) ne (wfLCon_le_id _)).
+        specialize (IHd1 (fun wl' f => P wl' (wfLCon_le_trans f Hinf))).
+        cbn in *.
+        pose proof (Hinf' := LCon_le_up (b := true) ne n0 f).
+        change (P (wl',,l (n0, true)) (Hinf' •ε Hinf)).
+        eapply IHd1 ; [now eauto |..].
+        intros wl'' f' Hover.
+        eapply H.
+        unshelve erewrite (decidInLCon_true _) ; [ | assumption].
+        now eapply f'; econstructor.
+      * pose proof (Hinf := LCon_le_step (l := k) (b := false) ne (wfLCon_le_id _)).
+        specialize (IHd2 (fun wl' f => P wl' (wfLCon_le_trans f Hinf))).
+        cbn in *.
+        pose proof (Hinf' := LCon_le_up (b := false) ne n0 f).
+        change (P (wl',,l (n0, false)) (Hinf' •ε Hinf)).
+        eapply IHd2 ; [now eauto |..].
+        intros wl'' f' Hover.
+        eapply H.
+        unshelve erewrite (decidInLCon_false _) ; [ | assumption].
+        now eapply f'; econstructor.
+Qed.        
+
 Section Typing.
 
   Context `{GenericTypingProperties}.