Prove injectivity of Pair and Lambdas

theories/fp_red.v

@@ -243,8 +243,45 @@ Module Pars.
       move => [b0 [h2 ?]]. subst.
       hauto lq:on rew:off ctrs:rtc.
   Qed.
+
+  #[local]Ltac solve_s_rec :=
+  move => *; eapply rtc_l; eauto;
+         hauto lq:on ctrs:Par.R use:Par.refl.
+
+  #[local]Ltac solve_s :=
+    repeat (induction 1; last by solve_s_rec); apply rtc_refl.
+
+  Lemma ProjCong n p (a0 a1 : Tm n) :
+    rtc Par.R a0 a1 ->
+    rtc Par.R (Proj p a0) (Proj p a1).
+  Proof. solve_s. Qed.
+
+  Lemma PairCong n (a0 a1 b0 b1 : Tm n) :
+    rtc Par.R a0 a1 ->
+    rtc Par.R b0 b1 ->
+    rtc Par.R (Pair a0 b0) (Pair a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma AppCong n (a0 a1 b0 b1 : Tm n) :
+    rtc Par.R a0 a1 ->
+    rtc Par.R b0 b1 ->
+    rtc Par.R (App a0 b0) (App a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma AbsCong n (a b : Tm (S n)) :
+    rtc Par.R a b ->
+    rtc Par.R (Abs a) (Abs b).
+  Proof. solve_s. Qed.
+
 End Pars.
 
+Definition var_or_bot {n} (a : Tm n) :=
+  match a with
+  | VarTm _ => true
+  | Bot => true
+  | _ => false
+  end.
+
 (***************** Beta rules only ***********************)
 Module RPar.
   Inductive R {n} : Tm n -> Tm n ->  Prop :=
@@ -373,8 +410,358 @@ Module RPar.
     move => h0 h1. apply morphing => //=.
     qauto l:on ctrs:R inv:option.
   Qed.
+
+  Lemma var_or_bot_imp {n} (a b : Tm n) :
+    var_or_bot a ->
+    a = b -> ~~ var_or_bot b -> False.
+  Proof.
+    hauto lq:on inv:Tm.
+  Qed.
+
+  Lemma var_or_bot_up n m (ρ : fin n -> Tm m) :
+    (forall i, var_or_bot (ρ i)) ->
+    (forall i, var_or_bot (up_Tm_Tm ρ i)).
+  Proof.
+    move => h /= [i|].
+    - asimpl.
+      move /(_ i) in h.
+      rewrite /funcomp.
+      move : (ρ i) h.
+      case => //=.
+    - sfirstorder.
+  Qed.
+
+  Local Ltac antiimp := qauto l:on use:var_or_bot_imp.
+
+  Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
+    (forall i, var_or_bot (ρ i)) ->
+    R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b.
+  Proof.
+    move E : (subst_Tm ρ a) => u hρ h.
+    move : n ρ hρ a E. elim : m u b/h.
+    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+               first by antiimp.
+      move => c c0 [+ ?]. subst.
+      case : c => //=; first by antiimp.
+      move => c [?]. subst.
+      spec_refl.
+      have /var_or_bot_up hρ' := hρ.
+      move : iha hρ' => /[apply] iha.
+      move : ihb hρ => /[apply] ihb.
+      spec_refl.
+      move : iha => [c1][ih0]?. subst.
+      move : ihb => [c2][ih1]?. subst.
+      eexists. split.
+      apply AppAbs; eauto.
+      by asimpl.
+    - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=;
+               first by antiimp.
+      move => []//=; first by antiimp.
+      move => t t0 t1 [*]. subst.
+      have  {}/iha := hρ => iha.
+      have  {}/ihb := hρ => ihb.
+      have  {}/ihc := hρ => ihc.
+      spec_refl.
+      move : iha => [? [*]].
+      move : ihb => [? [*]].
+      move : ihc => [? [*]].
+      eexists. split.
+      apply AppPair; hauto. subst.
+      by asimpl.
+    - move => n p a0 a1 ha iha m ρ hρ []//=;
+               first by antiimp.
+      move => p0 []//= t [*]; first by antiimp. subst.
+      have  /var_or_bot_up {}/iha  := hρ => iha.
+      spec_refl. move : iha => [b0 [? ?]]. subst.
+      eexists. split. apply ProjAbs; eauto. by asimpl.
+    - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+               first by antiimp.
+      move => p0 []//=; first by antiimp. move => t t0[*].
+      subst.
+      have {}/iha := (hρ) => iha.
+      have {}/ihb := (hρ) => ihb.
+      spec_refl.
+      move : iha => [b0 [? ?]].
+      move : ihb => [c0 [? ?]]. subst.
+      eexists. split. by eauto using ProjPair.
+      hauto q:on.
+    - move => n i m ρ hρ []//=.
+      hauto l:on.
+    - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp.
+      move => t [*]. subst.
+      have /var_or_bot_up {}/iha := hρ => iha.
+      spec_refl.
+      move  :iha => [b0 [? ?]]. subst.
+      eexists. split. by apply AbsCong; eauto.
+      by asimpl.
+    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+               first by antiimp.
+      move => t t0 [*]. subst.
+      have {}/iha := (hρ) => iha.
+      have {}/ihb := (hρ) => ihb.
+      spec_refl.
+      move : iha => [b0 [? ?]]. subst.
+      move : ihb => [c0 [? ?]]. subst.
+      eexists. split. by apply AppCong; eauto.
+      done.
+    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+               first by antiimp.
+      move => t t0[*]. subst.
+      have {}/iha := (hρ) => iha.
+      have {}/ihb := (hρ) => ihb.
+      spec_refl.
+      move : iha => [b0 [? ?]]. subst.
+      move : ihb => [c0 [? ?]]. subst.
+      eexists. split. by apply PairCong; eauto.
+      by asimpl.
+    - move => n p a0 a1 ha iha m ρ hρ []//=;
+               first by antiimp.
+      move => p0 t [*]. subst.
+      have {}/iha := (hρ) => iha.
+      spec_refl.
+      move : iha => [b0 [? ?]]. subst.
+      eexists. split. apply ProjCong; eauto. reflexivity.
+    - move => n p A0 A1 B0 B1 ha iha hB ihB m ρ hρ []//=;
+               first by antiimp.
+      move => ? t t0 [*]. subst.
+      have {}/iha := (hρ) => iha.
+      have /var_or_bot_up {}/ihB := (hρ) => ihB.
+      spec_refl.
+      move : iha => [b0 [? ?]].
+      move : ihB => [c0 [? ?]]. subst.
+      eexists. split. by apply BindCong; eauto.
+      by asimpl.
+    - hauto q:on ctrs:R inv:Tm.
+    - move => n i n0 ρ hρ []//=; first by antiimp.
+      hauto l:on.
+  Qed.
 End RPar.
 
+(***************** Beta rules only ***********************)
+Module RPar'.
+  Inductive R {n} : Tm n -> Tm n ->  Prop :=
+  (***************** Beta ***********************)
+  | AppAbs a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (App (Abs a0) b0)  (subst_Tm (scons b1 VarTm) a1)
+  | ProjPair p a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1)
+
+
+  (*************** Congruence ********************)
+  | Var i : R (VarTm i) (VarTm i)
+  | AbsCong a0 a1 :
+    R a0 a1 ->
+    R (Abs a0) (Abs a1)
+  | AppCong a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (App a0 b0) (App a1 b1)
+  | PairCong a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (Pair a0 b0) (Pair a1 b1)
+  | ProjCong p a0 a1 :
+    R a0 a1 ->
+    R (Proj p a0) (Proj p a1)
+  | BindCong p A0 A1 B0 B1:
+    R A0 A1 ->
+    R B0 B1 ->
+    R (TBind p A0 B0) (TBind p A1 B1)
+  | BotCong :
+    R Bot Bot
+  | UnivCong i :
+    R (Univ i) (Univ i).
+
+  Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
+
+  Lemma refl n (a : Tm n) : R a a.
+  Proof.
+    induction a; hauto lq:on ctrs:R.
+  Qed.
+
+  Lemma AppAbs' n a0 a1 (b0 b1 t : Tm n) :
+    t = subst_Tm (scons b1 VarTm) a1 ->
+    R a0 a1 ->
+    R b0 b1 ->
+    R (App (Abs a0) b0) t.
+  Proof. move => ->. apply AppAbs. Qed.
+
+  Lemma ProjPair' n p (a0 a1 b0 b1 : Tm n) t :
+    t = (if p is PL then a1 else b1) ->
+    R a0 a1 ->
+    R b0 b1 ->
+    R (Proj p (Pair a0 b0)) t.
+  Proof.  move => > ->. apply ProjPair. Qed.
+
+  Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) :
+    R a b -> R (ren_Tm ξ a) (ren_Tm ξ b).
+  Proof.
+    move => h. move : m ξ.
+    elim : n a b /h.
+    move => *; apply : AppAbs'; eauto; by asimpl.
+    all : qauto ctrs:R use:ProjPair'.
+  Qed.
+
+  Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> Tm m) (ξ : fin m -> fin p) :
+    (forall i, R (ρ0 i) (ρ1 i)) ->
+    (forall i, R ((funcomp (ren_Tm ξ) ρ0) i) ((funcomp (ren_Tm ξ) ρ1) i)).
+  Proof. eauto using renaming. Qed.
+
+  Lemma morphing_ext n m (ρ0 ρ1 : fin n -> Tm m) a b  :
+    R a b ->
+    (forall i, R (ρ0 i) (ρ1 i)) ->
+    (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)).
+  Proof. hauto q:on inv:option. Qed.
+
+  Lemma morphing_up n m (ρ0 ρ1 : fin n -> Tm m) :
+    (forall i, R (ρ0 i) (ρ1 i)) ->
+    (forall i, R (up_Tm_Tm ρ0 i) (up_Tm_Tm ρ1 i)).
+  Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_Tm_Tm. Qed.
+
+  Lemma morphing n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) :
+    (forall i, R (ρ0 i) (ρ1 i)) ->
+    R a b -> R (subst_Tm ρ0 a) (subst_Tm ρ1 b).
+  Proof.
+    move => + h. move : m ρ0 ρ1.
+    elim : n a b /h.
+    - move => *.
+      apply : AppAbs'; eauto using morphing_up.
+      by asimpl.
+    - hauto lq:on ctrs:R use:ProjPair' use:morphing_up.
+    - hauto lq:on ctrs:R use:morphing_up.
+    - hauto lq:on ctrs:R use:morphing_up.
+    - hauto lq:on ctrs:R use:morphing_up.
+    - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R use:morphing_up.
+    - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
+  Qed.
+
+  Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
+    R a b ->
+    R (subst_Tm ρ a) (subst_Tm ρ b).
+  Proof. hauto l:on use:morphing, refl. Qed.
+
+  Lemma cong n (a b : Tm (S n)) c d :
+    R a b ->
+    R c d ->
+    R (subst_Tm (scons c VarTm) a) (subst_Tm (scons d VarTm) b).
+  Proof.
+    move => h0 h1. apply morphing => //=.
+    qauto l:on ctrs:R inv:option.
+  Qed.
+
+  Lemma var_or_bot_imp {n} (a b : Tm n) :
+    var_or_bot a ->
+    a = b -> ~~ var_or_bot b -> False.
+  Proof.
+    hauto lq:on inv:Tm.
+  Qed.
+
+  Lemma var_or_bot_up n m (ρ : fin n -> Tm m) :
+    (forall i, var_or_bot (ρ i)) ->
+    (forall i, var_or_bot (up_Tm_Tm ρ i)).
+  Proof.
+    move => h /= [i|].
+    - asimpl.
+      move /(_ i) in h.
+      rewrite /funcomp.
+      move : (ρ i) h.
+      case => //=.
+    - sfirstorder.
+  Qed.
+
+  Local Ltac antiimp := qauto l:on use:var_or_bot_imp.
+
+  Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
+    (forall i, var_or_bot (ρ i)) ->
+    R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b.
+  Proof.
+    move E : (subst_Tm ρ a) => u hρ h.
+    move : n ρ hρ a E. elim : m u b/h.
+    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+               first by antiimp.
+      move => c c0 [+ ?]. subst.
+      case : c => //=; first by antiimp.
+      move => c [?]. subst.
+      spec_refl.
+      have /var_or_bot_up hρ' := hρ.
+      move : iha hρ' => /[apply] iha.
+      move : ihb hρ => /[apply] ihb.
+      spec_refl.
+      move : iha => [c1][ih0]?. subst.
+      move : ihb => [c2][ih1]?. subst.
+      eexists. split.
+      apply AppAbs; eauto.
+      by asimpl.
+    - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+               first by antiimp.
+      move => p0 []//=; first by antiimp. move => t t0[*].
+      subst.
+      have {}/iha := (hρ) => iha.
+      have {}/ihb := (hρ) => ihb.
+      spec_refl.
+      move : iha => [b0 [? ?]].
+      move : ihb => [c0 [? ?]]. subst.
+      eexists. split. by eauto using ProjPair.
+      hauto q:on.
+    - move => n i m ρ hρ []//=.
+      hauto l:on.
+    - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp.
+      move => t [*]. subst.
+      have /var_or_bot_up {}/iha := hρ => iha.
+      spec_refl.
+      move  :iha => [b0 [? ?]]. subst.
+      eexists. split. by apply AbsCong; eauto.
+      by asimpl.
+    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+               first by antiimp.
+      move => t t0 [*]. subst.
+      have {}/iha := (hρ) => iha.
+      have {}/ihb := (hρ) => ihb.
+      spec_refl.
+      move : iha => [b0 [? ?]]. subst.
+      move : ihb => [c0 [? ?]]. subst.
+      eexists. split. by apply AppCong; eauto.
+      done.
+    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+               first by antiimp.
+      move => t t0[*]. subst.
+      have {}/iha := (hρ) => iha.
+      have {}/ihb := (hρ) => ihb.
+      spec_refl.
+      move : iha => [b0 [? ?]]. subst.
+      move : ihb => [c0 [? ?]]. subst.
+      eexists. split. by apply PairCong; eauto.
+      by asimpl.
+    - move => n p a0 a1 ha iha m ρ hρ []//=;
+               first by antiimp.
+      move => p0 t [*]. subst.
+      have {}/iha := (hρ) => iha.
+      spec_refl.
+      move : iha => [b0 [? ?]]. subst.
+      eexists. split. apply ProjCong; eauto. reflexivity.
+    - move => n p A0 A1 B0 B1 ha iha hB ihB m ρ hρ []//=;
+               first by antiimp.
+      move => ? t t0 [*]. subst.
+      have {}/iha := (hρ) => iha.
+      have /var_or_bot_up {}/ihB := (hρ) => ihB.
+      spec_refl.
+      move : iha => [b0 [? ?]].
+      move : ihB => [c0 [? ?]]. subst.
+      eexists. split. by apply BindCong; eauto.
+      by asimpl.
+    - hauto q:on ctrs:R inv:Tm.
+    - move => n i n0 ρ hρ []//=; first by antiimp.
+      hauto l:on.
+  Qed.
+End RPar'.
+
 Module ERed.
   Inductive R {n} : Tm n -> Tm n ->  Prop :=
   (****************** Eta ***********************)
@@ -409,6 +796,8 @@ Module ERed.
     R B0 B1 ->
     R (TBind p A B0) (TBind p A B1).
 
+  Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
+
   Lemma AppEta' n a (u : Tm n) :
     u = (Abs (App (ren_Tm shift a) (VarTm var_zero))) ->
     R a u.
@@ -680,8 +1069,110 @@ Module RPars.
     rtc RPar.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b).
   Proof. hauto lq:on use:morphing inv:option. Qed.
 
+  Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
+    (forall i, var_or_bot (ρ i)) ->
+    rtc RPar.R (subst_Tm ρ a) b -> exists b0, rtc RPar.R a b0 /\ subst_Tm ρ b0 = b.
+  Proof.
+    move E  :(subst_Tm ρ a) => u hρ h.
+    move : a E.
+    elim : u b /h.
+    - sfirstorder.
+    - move => a b c h0 h1 ih1 a0 ?. subst.
+      move /RPar.antirenaming : h0.
+      move /(_ hρ).
+      move => [b0 [h2 ?]]. subst.
+      hauto lq:on rew:off ctrs:rtc.
+  Qed.
+
 End RPars.
 
+Module RPars'.
+
+  #[local]Ltac solve_s_rec :=
+  move => *; eapply rtc_l; eauto;
+         hauto lq:on ctrs:RPar'.R use:RPar'.refl.
+
+  #[local]Ltac solve_s :=
+    repeat (induction 1; last by solve_s_rec); apply rtc_refl.
+
+  Lemma AbsCong n (a b : Tm (S n)) :
+    rtc RPar'.R a b ->
+    rtc RPar'.R (Abs a) (Abs b).
+  Proof. solve_s. Qed.
+
+  Lemma AppCong n (a0 a1 b0 b1 : Tm n) :
+    rtc RPar'.R a0 a1 ->
+    rtc RPar'.R b0 b1 ->
+    rtc RPar'.R (App a0 b0) (App a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma BindCong n p (a0 a1 : Tm n) b0 b1 :
+    rtc RPar'.R a0 a1 ->
+    rtc RPar'.R b0 b1 ->
+    rtc RPar'.R (TBind p a0 b0) (TBind p a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma PairCong n (a0 a1 b0 b1 : Tm n) :
+    rtc RPar'.R a0 a1 ->
+    rtc RPar'.R b0 b1 ->
+    rtc RPar'.R (Pair a0 b0) (Pair a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma ProjCong n p (a0 a1  : Tm n) :
+    rtc RPar'.R a0 a1 ->
+    rtc RPar'.R (Proj p a0) (Proj p a1).
+  Proof. solve_s. Qed.
+
+  Lemma renaming n (a0 a1 : Tm n) m (ξ : fin n -> fin m) :
+    rtc RPar'.R a0 a1 ->
+    rtc RPar'.R (ren_Tm ξ a0) (ren_Tm ξ a1).
+  Proof.
+    induction 1.
+    - apply rtc_refl.
+    - eauto using RPar'.renaming, rtc_l.
+  Qed.
+
+  Lemma weakening n (a0 a1 : Tm n) :
+    rtc RPar'.R a0 a1 ->
+    rtc RPar'.R (ren_Tm shift a0) (ren_Tm shift a1).
+  Proof. apply renaming. Qed.
+
+  Lemma Abs_inv n (a : Tm (S n)) b :
+    rtc RPar'.R (Abs a) b -> exists a', b = Abs a' /\ rtc RPar'.R a a'.
+  Proof.
+    move E : (Abs a) => b0 h. move : a E.
+    elim : b0 b / h.
+    - hauto lq:on ctrs:rtc.
+    - hauto lq:on ctrs:rtc inv:RPar'.R, rtc.
+  Qed.
+
+  Lemma morphing n m (a b : Tm n) (ρ : fin n -> Tm m) :
+    rtc RPar'.R a b ->
+    rtc RPar'.R (subst_Tm ρ a) (subst_Tm ρ b).
+  Proof. induction 1; qauto l:on ctrs:rtc use:RPar'.substing. Qed.
+
+  Lemma substing n (a b : Tm (S n)) c :
+    rtc RPar'.R a b ->
+    rtc RPar'.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b).
+  Proof. hauto lq:on use:morphing inv:option. Qed.
+
+  Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
+    (forall i, var_or_bot (ρ i)) ->
+    rtc RPar'.R (subst_Tm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_Tm ρ b0 = b.
+  Proof.
+    move E  :(subst_Tm ρ a) => u hρ h.
+    move : a E.
+    elim : u b /h.
+    - sfirstorder.
+    - move => a b c h0 h1 ih1 a0 ?. subst.
+      move /RPar'.antirenaming : h0.
+      move /(_ hρ).
+      move => [b0 [h2 ?]]. subst.
+      hauto lq:on rew:off ctrs:rtc.
+  Qed.
+
+End RPars'.
+
 Lemma Abs_EPar n a (b : Tm n) :
   EPar.R (Abs a) b ->
   (exists d, EPar.R a d /\
@@ -1067,12 +1558,48 @@ Proof.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
 Qed.
 
+Function tstar' {n} (a : Tm n) :=
+  match a with
+  | VarTm i => a
+  | Abs a => Abs (tstar' a)
+  | App (Abs a) b => subst_Tm (scons (tstar' b) VarTm) (tstar' a)
+  | App a b => App (tstar' a) (tstar' b)
+  | Pair a b => Pair (tstar' a) (tstar' b)
+  | Proj p (Pair a b) => if p is PL then (tstar' a) else (tstar' b)
+  | Proj p a => Proj p (tstar' a)
+  | TBind p a b => TBind p (tstar' a) (tstar' b)
+  | Bot => Bot
+  | Univ i => Univ i
+  end.
+
+Lemma RPar'_triangle n (a : Tm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a).
+Proof.
+  apply tstar'_ind => {n a}.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on use:RPar'.cong, RPar'.refl ctrs:RPar'.R inv:RPar'.R.
+  - hauto lq:on rew:off ctrs:RPar'.R inv:RPar'.R.
+  - hauto lq:on rew:off inv:RPar'.R ctrs:RPar'.R.
+  - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'.
+  - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+Qed.
+
 Lemma RPar_diamond n (c a1 b1 : Tm n) :
   RPar.R c a1 ->
   RPar.R c b1 ->
   exists d2, RPar.R a1 d2 /\ RPar.R b1 d2.
 Proof. hauto l:on use:RPar_triangle. Qed.
 
+Lemma RPar'_diamond n (c a1 b1 : Tm n) :
+  RPar'.R c a1 ->
+  RPar'.R c b1 ->
+  exists d2, RPar'.R a1 d2 /\ RPar'.R b1 d2.
+Proof. hauto l:on use:RPar'_triangle. Qed.
+
 Lemma RPar_confluent n (c a1 b1 : Tm n) :
   rtc RPar.R c a1 ->
   rtc RPar.R c b1 ->
@@ -1269,15 +1796,13 @@ Qed.
 Lemma prov_pair n (u : Tm n) a : prov u a <-> prov u (Pair (Proj PL a) (Proj PR a)).
 Proof. hauto lq:on inv:prov ctrs:prov. Qed.
 
-Derive Dependent Inversion inv with (forall n (a b : Tm n), ERed.R a b) Sort Prop.
-
 Lemma prov_ered n (u : Tm n) a b : prov u a -> ERed.R a b -> prov u b.
 Proof.
   move => h.
   move : b.
   elim : u a / h.
   - move => p A A0 B B0 hA hB b.
-    elim /inv => // _.
+    elim /ERed.inv => // _.
     + move => a0 *. subst.
       rewrite -prov_lam.
       by constructor.
@@ -1287,7 +1812,7 @@ Proof.
     + qauto l:on ctrs:prov use:@rtc_r, ERed_EPar, EPar_Par.
     + qauto l:on ctrs:prov use:@rtc_r, ERed_EPar, EPar_Par.
   - move => h a ha iha b.
-    elim /inv => // _.
+    elim /ERed.inv => // _.
     + move => a0 *. subst.
       rewrite -prov_lam.
       by constructor.
@@ -1297,7 +1822,7 @@ Proof.
     + hauto lq:on ctrs:prov use:ERed.substing.
   - hauto lq:on inv:ERed.R, prov ctrs:prov.
   - move => h a b ha iha hb ihb b0.
-    elim /inv => //_.
+    elim /ERed.inv => //_.
     + move => a0 *. subst.
       rewrite -prov_lam.
       by constructor.
@@ -1371,6 +1896,7 @@ Definition prov_extract_spec {n} u (a : Tm n) :=
   | TBind p A B => exists A0 B0, extract a = TBind p A0 B0 /\ rtc Par.R A A0 /\ rtc Par.R B B0
   | Univ i => extract a = Univ i
   | VarTm i => extract a = VarTm i
+  | Bot => extract a = Bot
   | _ => True
   end.
 
@@ -1391,6 +1917,8 @@ Proof.
       rewrite ren_subst_bot in h0.
       rewrite h0.
       eauto.
+    + move => _ /(_ Bot).
+      by rewrite ren_subst_bot.
     + move => i h /(_ Bot).
       by rewrite ren_subst_bot => ->.
   - hauto lq:on.
@@ -1863,8 +2391,222 @@ Proof.
   hauto l:on.
 Qed.
 
-
 Lemma join_substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
   join a b ->
   join (subst_Tm ρ a) (subst_Tm ρ b).
 Proof. hauto lq:on unfold:join use:Pars.substing. Qed.
+
+Fixpoint ne {n} (a : Tm n) :=
+  match a with
+  | VarTm i => true
+  | TBind _ A B => false
+  | Bot => true
+  | App a b => ne a && nf b
+  | Abs a => false
+  | Univ _ => false
+  | Proj _ a => ne a
+  | Pair _ _ => false
+  end
+with nf {n} (a : Tm n) :=
+  match a with
+  | VarTm i => true
+  | TBind _ A B => nf A && nf B
+  | Bot => true
+  | App a b => ne a && nf b
+  | Abs a => nf a
+  | Univ _ => true
+  | Proj _ a => ne a
+  | Pair a b => nf a && nf b
+end.
+
+Lemma ne_nf n a : @ne n a -> nf a.
+Proof. elim : a => //=. Qed.
+
+Definition wn {n} (a : Tm n) := exists b, rtc RPar'.R a b /\ nf b.
+Definition wne {n} (a : Tm n) := exists b, rtc RPar'.R a b /\ ne b.
+
+(* Weakly neutral implies weakly normal *)
+Lemma wne_wn n a : @wne n a -> wn a.
+Proof. sfirstorder use:ne_nf. Qed.
+
+(* Normal implies weakly normal *)
+Lemma nf_wn n v : @nf n v -> wn v.
+Proof. sfirstorder ctrs:rtc. Qed.
+
+Lemma nf_refl n (a b : Tm n) (h : RPar'.R a b) : (nf a -> b = a) /\ (ne a -> b = a).
+Proof.
+  elim : a b /h => //=; solve [hauto b:on].
+Qed.
+
+Lemma ne_nf_ren n m (a : Tm n) (ξ : fin n -> fin m) :
+  (ne a <-> ne (ren_Tm ξ a)) /\ (nf a <-> nf (ren_Tm ξ a)).
+Proof.
+  move : m ξ. elim : n / a => //=; solve [hauto b:on].
+Qed.
+
+Lemma wne_app n (a b : Tm n) :
+  wne a -> wn b -> wne (App a b).
+Proof.
+  move => [a0 [? ?]] [b0 [? ?]].
+  exists (App a0 b0). hauto b:on drew:off use:RPars'.AppCong.
+Qed.
+
+Lemma wn_abs n a (h : wn a) : @wn n (Abs a).
+Proof.
+  move : h => [v [? ?]].
+  exists (Abs v).
+  eauto using RPars'.AbsCong.
+Qed.
+
+Lemma wn_bind n p A B : wn A -> wn B -> wn (@TBind n p A B).
+Proof.
+  move => [A0 [? ?]] [B0 [? ?]].
+  exists (TBind p A0 B0).
+  hauto lqb:on use:RPars'.BindCong.
+Qed.
+
+Lemma wn_pair n (a b : Tm n) : wn a -> wn b -> wn (Pair a b).
+Proof.
+  move => [a0 [? ?]] [b0 [? ?]].
+  exists (Pair a0 b0).
+  hauto lqb:on use:RPars'.PairCong.
+Qed.
+
+Lemma wne_proj n p (a : Tm n) : wne a -> wne (Proj p a).
+Proof.
+  move => [a0 [? ?]].
+  exists (Proj p a0). hauto lqb:on use:RPars'.ProjCong.
+Qed.
+
+Create HintDb nfne.
+#[export]Hint Resolve nf_wn ne_nf wne_wn nf_refl : nfne.
+
+Lemma ne_nf_antiren n m (a : Tm n) (ρ : fin n -> Tm m) :
+  (forall i, var_or_bot (ρ i)) ->
+  (ne (subst_Tm ρ a) -> ne a) /\ (nf (subst_Tm ρ a) -> nf a).
+Proof.
+  move : m ρ. elim : n / a => //;
+   hauto b:on drew:off use:RPar.var_or_bot_up.
+Qed.
+
+Lemma wn_antirenaming n m a (ρ : fin n -> Tm m) :
+  (forall i, var_or_bot (ρ i)) ->
+  wn (subst_Tm ρ a) -> wn a.
+Proof.
+  rewrite /wn => hρ.
+  move => [v [rv nfv]].
+  move /RPars'.antirenaming : rv.
+  move /(_ hρ) => [b [hb ?]]. subst.
+  exists b. split => //=.
+  move : nfv.
+  by eapply ne_nf_antiren.
+Qed.
+
+Lemma ext_wn n (a : Tm n) :
+    wn (App a Bot) ->
+    wn a.
+Proof.
+  move E : (App a Bot) => a0 [v [hr hv]].
+  move : a E.
+  move : hv.
+  elim : a0 v / hr.
+  - hauto q:on inv:Tm ctrs:rtc b:on db: nfne.
+  - move => a0 a1 a2 hr0 hr1 ih hnfa2.
+    move /(_ hnfa2) in ih.
+    move => a.
+    case : a0 hr0=>// => b0 b1.
+    elim /RPar'.inv=>// _.
+    + move => a0 a3 b2 b3 ? ? [? ?] ? [? ?]. subst.
+      have ? : b3 = Bot by hauto lq:on inv:RPar'.R. subst.
+      suff : wn (Abs a3) by hauto lq:on ctrs:RPar'.R, rtc unfold:wn.
+      have : wn (subst_Tm (scons Bot VarTm) a3) by sfirstorder.
+      move => h. apply wn_abs.
+      move : h. apply wn_antirenaming.
+      hauto lq:on rew:off inv:option.
+    + hauto q:on inv:RPar'.R ctrs:rtc b:on.
+Qed.
+
+Module Join.
+  Lemma ProjCong p n (a0 a1 : Tm n) :
+    join a0 a1 ->
+    join (Proj p a0) (Proj p a1).
+  Proof. hauto lq:on use:Pars.ProjCong unfold:join. Qed.
+
+  Lemma PairCong n (a0 a1 b0 b1 : Tm n) :
+    join a0 a1 ->
+    join b0 b1 ->
+    join (Pair a0 b0) (Pair a1 b1).
+  Proof. hauto lq:on use:Pars.PairCong unfold:join. Qed.
+
+  Lemma AppCong n (a0 a1 b0 b1 : Tm n) :
+    join a0 a1 ->
+    join b0 b1 ->
+    join (App a0 b0) (App a1 b1).
+  Proof. hauto lq:on use:Pars.AppCong. Qed.
+
+  Lemma AbsCong n (a b : Tm (S n)) :
+    join a b ->
+    join (Abs a) (Abs b).
+  Proof. hauto lq:on use:Pars.AbsCong. Qed.
+
+  Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) :
+    join a b -> join (ren_Tm ξ a) (ren_Tm ξ b).
+  Proof.
+    induction 1; hauto lq:on use:Pars.renaming.
+  Qed.
+
+  Lemma weakening n (a b : Tm n)  :
+    join a b -> join (ren_Tm shift a) (ren_Tm shift b).
+  Proof.
+    apply renaming.
+  Qed.
+
+  Lemma FromPar n (a b : Tm n) :
+    Par.R a b ->
+    join a b.
+  Proof.
+    hauto lq:on ctrs:rtc use:rtc_once.
+  Qed.
+End Join.
+
+Lemma abs_eq n a (b : Tm n) :
+  join (Abs a) b <-> join a (App (ren_Tm shift b) (VarTm var_zero)).
+Proof.
+  split.
+  - move => /Join.weakening h.
+    have {h} : join (App (ren_Tm shift (Abs a)) (VarTm var_zero)) (App (ren_Tm shift b) (VarTm var_zero))
+      by hauto l:on use:Join.AppCong, join_refl.
+    simpl.
+    move => ?. apply : join_transitive; eauto.
+    apply join_symmetric. apply Join.FromPar.
+    apply : Par.AppAbs'; eauto using Par.refl. by asimpl.
+  - move /Join.AbsCong.
+    move /join_transitive. apply.
+    apply join_symmetric. apply Join.FromPar. apply Par.AppEta. apply Par.refl.
+Qed.
+
+Lemma pair_eq n (a0 a1 b : Tm n) :
+  join (Pair a0 a1) b <-> join a0 (Proj PL b) /\ join a1 (Proj PR b).
+Proof.
+  split.
+  - move => h.
+    have /Join.ProjCong {}h := h.
+    have h0 : forall p, join (if p is PL then a0 else a1) (Proj p (Pair a0 a1))
+                     by hauto lq:on use:join_symmetric, Join.FromPar, Par.ProjPair', Par.refl.
+    hauto lq:on rew:off use:join_transitive, join_symmetric.
+  - move => [h0 h1].
+    move : h0 h1.
+    move : Join.PairCong; repeat move/[apply].
+    move /join_transitive. apply. apply join_symmetric.
+    apply Join.FromPar. hauto lq:on ctrs:Par.R use:Par.refl.
+Qed.
+
+Lemma join_pair_inj n (a0 a1 b0 b1 : Tm n) :
+  join (Pair a0 a1) (Pair b0 b1) <-> join a0 b0 /\ join a1 b1.
+Proof.
+  split; last by hauto lq:on use:Join.PairCong.
+  move /pair_eq => [h0 h1].
+  have : join (Proj PL (Pair b0 b1)) b0 by hauto lq:on use:Join.FromPar, Par.refl, Par.ProjPair'.
+  have : join (Proj PR (Pair b0 b1)) b1 by hauto lq:on use:Join.FromPar, Par.refl, Par.ProjPair'.
+  eauto using join_transitive.
+Qed.

theories/logrel.v

@@ -6,18 +6,22 @@ Require Import ssreflect ssrbool.
 Require Import Logic.PropExtensionality (propositional_extensionality).
 From stdpp Require Import relations (rtc(..), rtc_subrel).
 Import Psatz.
-Definition ProdSpace (PA : Tm 0 -> Prop)
-  (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop) b : Prop :=
+
+Definition ProdSpace {n} (PA : Tm n -> Prop)
+  (PF : Tm n -> (Tm n -> Prop) -> Prop) b : Prop :=
   forall a PB, PA a -> PF a PB -> PB (App b a).
 
-Definition SumSpace (PA : Tm 0 -> Prop)
-  (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop) t : Prop :=
-  exists a b, rtc RPar.R t (Pair a b) /\ PA a /\ (forall PB, PF a PB -> PB b).
+Definition SumSpace {n} (PA : Tm n -> Prop)
+  (PF : Tm n -> (Tm n -> Prop) -> Prop) t : Prop :=
+  wne t \/ exists a b, rtc RPar'.R t (Pair a b) /\ PA a /\ (forall PB, PF a PB -> PB b).
 
-Definition BindSpace p := if p is TPi then ProdSpace else SumSpace.
+Definition BindSpace {n} p := if p is TPi then @ProdSpace n else SumSpace.
 
 Reserved Notation "⟦ A ⟧ i ;; I ↘ S" (at level 70).
-Inductive InterpExt i (I : nat -> Tm 0 -> Prop) : Tm 0 -> (Tm 0 -> Prop) -> Prop :=
+Inductive InterpExt {n} i (I : nat -> Tm n -> Prop) : Tm n -> (Tm n -> Prop) -> Prop :=
+| InterpExt_Ne A :
+  ne A ->
+  ⟦ A ⟧ i ;; I ↘ wne
 | InterpExt_Bind p A B PA PF :
   ⟦ A ⟧ i ;; I ↘ PA ->
   (forall a, PA a -> exists PB, PF a PB) ->
@@ -29,12 +33,12 @@ Inductive InterpExt i (I : nat -> Tm 0 -> Prop) : Tm 0 -> (Tm 0 -> Prop) -> Prop
   ⟦ Univ j ⟧ i ;; I ↘ (I j)
 
 | InterpExt_Step A A0 PA :
-  RPar.R A A0 ->
+  RPar'.R A A0 ->
   ⟦ A0 ⟧ i ;; I ↘ PA ->
   ⟦ A ⟧ i ;; I ↘ PA
 where "⟦ A ⟧ i ;; I ↘ S" := (InterpExt i I A S).
 
-Lemma InterpExt_Univ'  i  I j (PF : Tm 0 -> Prop) :
+Lemma InterpExt_Univ' n i  I j (PF : Tm n -> Prop) :
   PF = I j ->
   j < i ->
   ⟦ Univ j ⟧ i ;; I ↘ PF.
@@ -42,28 +46,29 @@ Proof. hauto lq:on ctrs:InterpExt. Qed.
 
 Infix "<?" := Compare_dec.lt_dec (at level 60).
 
-Equations InterpUnivN (i : nat) : Tm 0 -> (Tm 0 -> Prop) -> Prop by wf i lt :=
-  InterpUnivN i := @InterpExt i
+Equations InterpUnivN n (i : nat) : Tm n -> (Tm n -> Prop) -> Prop by wf i lt :=
+  InterpUnivN n i := @InterpExt n i
                      (fun j A =>
                         match j <? i  with
-                        | left _ => exists PA, InterpUnivN  j A PA
+                        | left _ => exists PA, InterpUnivN n j A PA
                         | right _ => False
                         end).
-Arguments InterpUnivN .
+Arguments InterpUnivN {n}.
 
-Lemma InterpExt_lt_impl i I I' A (PA : Tm 0 -> Prop) :
+Lemma InterpExt_lt_impl n i I I' A (PA : Tm n -> Prop) :
   (forall j, j < i -> I j = I' j) ->
   ⟦ A ⟧ i ;; I ↘ PA ->
   ⟦ A ⟧ i ;; I' ↘ PA.
 Proof.
   move => hI h.
   elim : A PA /h.
+  - hauto q:on ctrs:InterpExt.
   - hauto lq:on rew:off ctrs:InterpExt.
   - hauto q:on ctrs:InterpExt.
   - hauto lq:on ctrs:InterpExt.
 Qed.
 
-Lemma InterpExt_lt_eq i I I' A (PA : Tm 0 -> Prop) :
+Lemma InterpExt_lt_eq n i I I' A (PA : Tm n -> Prop) :
   (forall j, j < i -> I j = I' j) ->
   ⟦ A ⟧ i ;; I ↘ PA =
   ⟦ A ⟧ i ;; I' ↘ PA.
@@ -75,8 +80,8 @@ Qed.
 
 Notation "⟦ A ⟧ i ↘ S" := (InterpUnivN i A S) (at level 70).
 
-Lemma InterpUnivN_nolt i :
-  InterpUnivN i = InterpExt i (fun j (A : Tm 0) => exists PA, ⟦ A ⟧ j ↘ PA).
+Lemma InterpUnivN_nolt n i :
+  @InterpUnivN n i = @InterpExt n i (fun j (A : Tm n) => exists PA, ⟦ A ⟧ j ↘ PA).
 Proof.
   simp InterpUnivN.
   extensionality A. extensionality PA.
@@ -89,12 +94,12 @@ Qed.
 #[export]Hint Rewrite @InterpUnivN_nolt : InterpUniv.
 
 Lemma RPar_substone n (a b : Tm (S n)) (c : Tm n):
-    RPar.R a b -> RPar.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b).
-  Proof. hauto l:on inv:option use:RPar.substing, RPar.refl. Qed.
+    RPar'.R a b -> RPar'.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b).
+  Proof. hauto l:on inv:option use:RPar'.substing, RPar'.refl. Qed.
 
-Lemma InterpExt_Bind_inv p i I (A : Tm 0) B P
+Lemma InterpExt_Bind_inv n p i I (A : Tm n) B P
   (h :  ⟦ TBind p A B ⟧ i ;; I ↘ P) :
-  exists (PA : Tm 0 -> Prop) (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop),
+  exists (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop),
      ⟦ A ⟧ i ;; I ↘ PA /\
     (forall a, PA a -> exists PB, PF a PB) /\
     (forall a PB, PF a PB -> ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) /\
@@ -103,24 +108,35 @@ Proof.
   move E : (TBind p A B) h => T h.
   move : A B E.
   elim : T P / h => //.
+  - move => //= *. scongruence.
   - hauto l:on.
   - move => A A0 PA hA hA0 hPi A1 B ?. subst.
-    elim /RPar.inv : hA => //= _ p0 A2 A3 B0 B1 hA1 hB0 [*]. subst.
+    elim /RPar'.inv : hA => //= _ p0 A2 A3 B0 B1 hA1 hB0 [*]. subst.
     hauto lq:on ctrs:InterpExt use:RPar_substone.
 Qed.
 
-Lemma InterpExt_Univ_inv i I j P
-  (h :  ⟦ Univ j  ⟧ i ;; I ↘ P) :
+Lemma InterpExt_Ne_inv n i A I P
+  (h :  ⟦ A : Tm n  ⟧ i ;; I ↘ P) :
+  ne A ->
+  P = wne.
+Proof.
+  elim : A P / h => //=.
+  qauto l:on ctrs:prov inv:prov use:nf_refl.
+Qed.
+
+Lemma InterpExt_Univ_inv n i I j P
+  (h :  ⟦ Univ j : Tm n  ⟧ i ;; I ↘ P) :
   P = I j /\ j < i.
 Proof.
   move : h.
   move E : (Univ j) => T h. move : j E.
   elim : T P /h => //.
+  - move => //= *. scongruence.
   - hauto l:on.
-  - hauto lq:on rew:off inv:RPar.R.
+  - hauto lq:on rew:off inv:RPar'.R.
 Qed.
 
-Lemma InterpExt_Bind_nopf p i I (A : Tm 0) B PA  :
+Lemma InterpExt_Bind_nopf n p i I (A : Tm n) B PA  :
   ⟦ A ⟧ i ;; I ↘ PA ->
   (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘  PB) ->
   ⟦ TBind p A B ⟧ i ;; I ↘ (BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB)).
@@ -128,7 +144,7 @@ Proof.
   move => h0 h1. apply InterpExt_Bind =>//.
 Qed.
 
-Lemma InterpUnivN_Fun_nopf p i (A : Tm 0) B PA :
+Lemma InterpUnivN_Fun_nopf n p i (A : Tm n) B PA :
   ⟦ A ⟧ i ↘ PA ->
   (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) ->
   ⟦ TBind p A B ⟧ i ↘ (BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB)).
@@ -136,7 +152,7 @@ Proof.
   hauto l:on use:InterpExt_Bind_nopf rew:db:InterpUniv.
 Qed.
 
-Lemma InterpExt_cumulative i j I (A : Tm 0) PA :
+Lemma InterpExt_cumulative n i j I (A : Tm n) PA :
   i <= j ->
    ⟦ A ⟧ i ;; I ↘ PA ->
    ⟦ A ⟧ j ;; I ↘ PA.
@@ -146,61 +162,87 @@ Proof.
     hauto l:on ctrs:InterpExt solve+:(by lia).
 Qed.
 
-Lemma InterpUnivN_cumulative i (A : Tm 0) PA :
+Lemma InterpUnivN_cumulative n i (A : Tm n) PA :
    ⟦ A ⟧ i ↘ PA -> forall j, i <= j ->
    ⟦ A ⟧ j ↘ PA.
 Proof.
   hauto l:on rew:db:InterpUniv use:InterpExt_cumulative.
 Qed.
 
-Lemma InterpExt_preservation i I (A : Tm 0) B P (h : InterpExt i I A P) :
-  RPar.R A B ->
+Lemma InterpExt_preservation n i I (A : Tm n) B P (h : InterpExt i I A P) :
+  RPar'.R A B ->
   ⟦ B ⟧ i ;; I ↘ P.
 Proof.
   move : B.
   elim : A P / h; auto.
+  - hauto lq:on use:nf_refl ctrs:InterpExt.
   - move => p A B PA PF hPA ihPA hPB hPB' ihPB T hT.
-    elim /RPar.inv :  hT => //.
+    elim /RPar'.inv :  hT => //.
     move => hPar p0 A0 A1 B0 B1 h0 h1 [? ?] ? ?; subst.
     apply InterpExt_Bind; auto => a PB hPB0.
     apply : ihPB; eauto.
-    sfirstorder use:RPar.cong, RPar.refl.
-  - hauto lq:on inv:RPar.R ctrs:InterpExt.
+    sfirstorder use:RPar'.cong, RPar'.refl.
+  - hauto lq:on inv:RPar'.R ctrs:InterpExt.
   - move => A B P h0 h1 ih1 C hC.
-    have [D [h2 h3]] := RPar_diamond  _ _ _ _ h0 hC.
+    have [D [h2 h3]] := RPar'_diamond  _ _ _ _ h0 hC.
     hauto lq:on ctrs:InterpExt.
 Qed.
 
-Lemma InterpUnivN_preservation i (A : Tm 0) B P (h : ⟦ A ⟧ i ↘ P) :
-  RPar.R A B ->
+Lemma InterpUnivN_preservation n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) :
+  RPar'.R A B ->
   ⟦ B ⟧ i ↘ P.
 Proof. hauto l:on rew:db:InterpUnivN use: InterpExt_preservation. Qed.
 
-Lemma InterpExt_back_preservation_star i I (A : Tm 0) B P (h : ⟦ B ⟧ i ;; I ↘ P) :
-  rtc RPar.R A B ->
+Lemma InterpExt_back_preservation_star n i I (A : Tm n) B P (h : ⟦ B ⟧ i ;; I ↘ P) :
+  rtc RPar'.R A B ->
   ⟦ A ⟧ i ;; I ↘ P.
 Proof. induction 1; hauto l:on ctrs:InterpExt. Qed.
 
-Lemma InterpExt_preservation_star i I (A : Tm 0) B P (h : ⟦ A ⟧ i ;; I ↘ P) :
-  rtc RPar.R A B ->
+Lemma InterpExt_preservation_star n i I (A : Tm n) B P (h : ⟦ A ⟧ i ;; I ↘ P) :
+  rtc RPar'.R A B ->
   ⟦ B ⟧ i ;; I ↘ P.
 Proof. induction 1; hauto l:on use:InterpExt_preservation. Qed.
 
-Lemma InterpUnivN_preservation_star i (A : Tm 0) B P (h : ⟦ A ⟧ i ↘ P) :
-  rtc RPar.R A B ->
+Lemma InterpUnivN_preservation_star n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) :
+  rtc RPar'.R A B ->
   ⟦ B ⟧ i ↘ P.
 Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_preservation_star. Qed.
 
-Lemma InterpUnivN_back_preservation_star i (A : Tm 0) B P (h : ⟦ B ⟧ i ↘ P) :
-  rtc RPar.R A B ->
+Lemma InterpUnivN_back_preservation_star n i (A : Tm n) B P (h : ⟦ B ⟧ i ↘ P) :
+  rtc RPar'.R A B ->
   ⟦ A ⟧ i ↘ P.
 Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_back_preservation_star. Qed.
 
-Lemma InterpExtInv i I (A : Tm 0) PA :
+Function hfb {n} (A : Tm n) :=
+  match A with
+  | TBind _ _ _ => true
+  | Univ _ => true
+  | _ => ne A
+  end.
+
+Inductive hfb_case {n} : Tm n -> Prop :=
+| hfb_bind p A B :
+  hfb_case (TBind p A B)
+| hfb_univ i :
+  hfb_case (Univ i)
+| hfb_ne A :
+  ne A ->
+  hfb_case A.
+
+Derive Dependent Inversion hfb_inv with (forall n (a : Tm n), hfb_case a) Sort Prop.
+
+Lemma ne_hfb {n} (A : Tm n) : ne A -> hfb A.
+Proof. case : A => //=. Qed.
+
+Lemma hfb_caseP {n} (A : Tm n) : hfb A -> hfb_case A.
+Proof. hauto lq:on ctrs:hfb_case inv:Tm use:ne_hfb. Qed.
+
+Lemma InterpExtInv n i I (A : Tm n) PA :
   ⟦ A ⟧ i ;; I ↘ PA ->
-  exists B, hfb B /\ rtc RPar.R A B /\  ⟦ B ⟧ i ;; I ↘ PA.
+  exists B, hfb B /\ rtc RPar'.R A B /\  ⟦ B ⟧ i ;; I ↘ PA.
 Proof.
   move => h. elim : A PA /h.
+  - hauto q:on ctrs:InterpExt, rtc use:ne_hfb.
   - move => p A B PA PF hPA _ hPF hPF0 _.
     exists (TBind p A B). repeat split => //=.
     apply rtc_refl.
@@ -210,17 +252,22 @@ Proof.
   - hauto lq:on ctrs:rtc.
 Qed.
 
-Lemma RPars_Pars  (A B : Tm 0) :
-  rtc RPar.R A B ->
+Lemma RPar'_Par n (A B : Tm n) :
+  RPar'.R A B ->
+  Par.R A B.
+Proof. induction 1; hauto lq:on ctrs:Par.R. Qed.
+
+Lemma RPar's_Pars n (A B : Tm n) :
+  rtc RPar'.R A B ->
   rtc Par.R A B.
-Proof. hauto lq:on use:RPar_Par, rtc_subrel. Qed.
+Proof. hauto lq:on use:RPar'_Par, rtc_subrel. Qed.
 
-Lemma RPars_join  (A B : Tm 0) :
-  rtc RPar.R A B -> join A B.
-Proof. hauto lq:on ctrs:rtc use:RPars_Pars. Qed.
+Lemma RPar's_join n (A B : Tm n) :
+  rtc RPar'.R A B -> join A B.
+Proof. hauto lq:on ctrs:rtc use:RPar's_Pars. Qed.
 
-Lemma bindspace_iff  p (PA : Tm 0 -> Prop) PF PF0 b  :
-  (forall (a : Tm 0) (PB PB0 : Tm 0 -> Prop), PF a PB -> PF0 a PB0 -> PB = PB0) ->
+Lemma bindspace_iff n p (PA : Tm n -> Prop) PF PF0 b  :
+  (forall (a : Tm n) (PB PB0 : Tm n -> Prop), PF a PB -> PF0 a PB0 -> PB = PB0) ->
   (forall a, PA a -> exists PB, PF a PB) ->
   (forall a, PA a -> exists PB0, PF0 a PB0) ->
   (BindSpace p PA PF b <-> BindSpace p PA PF0 b).
@@ -241,21 +288,76 @@ Proof.
     hauto lq:on rew:off.
 Qed.
 
-Lemma InterpExt_Join i I (A B : Tm 0) PA PB :
+Lemma ne_prov_inv n (a : Tm n) :
+  ne a -> (exists i, prov (VarTm i) a) \/ prov Bot a.
+Proof.
+  elim : n /a => //=.
+  - hauto lq:on ctrs:prov.
+  - hauto lq:on rew:off ctrs:prov b:on.
+  - hauto lq:on ctrs:prov.
+  - move => n.
+    have : @prov n Bot Bot by auto using P_Bot.
+    tauto.
+Qed.
+
+Lemma ne_pars_inv n (a b : Tm n) :
+  ne a -> rtc Par.R a b -> (exists i, prov (VarTm i) b) \/ prov Bot b.
+Proof.
+  move /ne_prov_inv.
+  sfirstorder use:prov_pars.
+Qed.
+
+Lemma ne_pars_extract  n (a b : Tm n) :
+  ne a -> rtc Par.R a b -> (exists i, extract b = (VarTm i)) \/ extract b = Bot.
+Proof. hauto lq:on rew:off use:ne_pars_inv, prov_extract. Qed.
+
+Lemma join_bind_ne_contra n p (A : Tm n) B C :
+  ne C ->
+  join (TBind p A B) C -> False.
+Proof.
+  move => hC [D [h0 h1]].
+  move /pars_pi_inv : h0 => [A0 [B0 [h2 [h3 h4]]]].
+  have : (exists i, extract D = (VarTm i)) \/ extract D = Bot by eauto using ne_pars_extract.
+  sfirstorder.
+Qed.
+
+Lemma join_univ_ne_contra n i C :
+  ne C ->
+  join (Univ i : Tm n) C -> False.
+Proof.
+  move => hC [D [h0 h1]].
+  move /pars_univ_inv : h0 => ?.
+  have : (exists i, extract D = (VarTm i)) \/ extract D = Bot by eauto using ne_pars_extract.
+  sfirstorder.
+Qed.
+
+#[export]Hint Resolve join_univ_ne_contra join_bind_ne_contra join_univ_pi_contra join_symmetric join_transitive : join.
+
+Lemma InterpExt_Join n i I (A B : Tm n) PA PB :
   ⟦ A ⟧ i ;; I ↘ PA ->
   ⟦ B ⟧ i ;; I ↘ PB ->
   join A B ->
   PA = PB.
 Proof.
   move => h. move : B PB. elim : A PA /h.
+  - move => A hA B PB /InterpExtInv.
+    move => [B0 []].
+    move /hfb_caseP. elim/hfb_inv => _.
+    + move => p A0 B1 ? [/RPar's_join h0 h1] h2. subst. exfalso.
+      eauto with join.
+    + move => ? ? [/RPar's_join *]. subst. exfalso.
+      eauto with join.
+    + hauto lq:on use:InterpExt_Ne_inv.
   - move => p A B PA PF hPA ihPA hTot hRes ihPF U PU /InterpExtInv.
     move => [B0 []].
-    case : B0 => //=.
-    + move => p0 A0 B0 _ [hr hPi].
+    move /hfb_caseP.
+    elim /hfb_inv => _.
+    rename B0 into B00.
+    + move => p0 A0 B0 ?  [hr hPi]. subst.
       move /InterpExt_Bind_inv : hPi.
       move => [PA0][PF0][hPA0][hTot0][hRes0]?. subst.
       move => hjoin.
-      have{}hr : join U (TBind p0 A0 B0) by auto using RPars_join.
+      have{}hr : join U (TBind p0 A0 B0) by auto using RPar's_join.
       have hj : join (TBind p A B) (TBind p0 A0 B0) by eauto using join_transitive.
       have {hj} : p0 = p /\ join A A0 /\ join B B0 by hauto l:on use:join_pi_inj.
       move => [? [h0 h1]]. subst.
@@ -267,62 +369,64 @@ Proof.
       move => a PB PB0 hPB hPB0.
       apply : ihPF; eauto.
       by apply join_substing.
-    + move => j _.
+    + move => j ?. subst.
       move => [h0 h1] h.
-      have ? : join U (Univ j) by eauto using RPars_join.
+      have ? : join U (Univ j) by eauto using RPar's_join.
       have : join (TBind p A B) (Univ j) by eauto using join_transitive.
       move => ?. exfalso.
       eauto using join_univ_pi_contra.
+    + move => A0 ? ? [/RPar's_join ?]. subst.
+      move => _ ?. exfalso. eauto with join.
   - move => j ? B PB /InterpExtInv.
-    move => [+ []]. case => //=.
+    move => [? []]. move/hfb_caseP.
+    elim /hfb_inv => //= _.
     + move => p A0 B0 _ [].
-      move /RPars_join => *.
-      have ?  : join (TBind p A0 B0) (Univ j) by eauto using join_symmetric, join_transitive.
-      exfalso.
-      eauto using join_univ_pi_contra.
-    + move => m _ [/RPars_join h0 + h1].
-      have /join_univ_inj {h0 h1} ?  : join (Univ j : Tm 0) (Univ m) by eauto using join_transitive.
+      move /RPar's_join => *.
+      exfalso. eauto with join.
+    + move => m _ [/RPar's_join h0 + h1].
+      have /join_univ_inj {h0 h1} ?  : join (Univ j : Tm n) (Univ m) by eauto using join_transitive.
       subst.
       move /InterpExt_Univ_inv. firstorder.
+    + move => A ? ? [/RPar's_join] *. subst. exfalso. eauto with join.
   - move => A A0 PA h.
-    have /join_symmetric {}h : join A A0 by hauto lq:on ctrs:rtc use:RPar_Par, relations.rtc_once.
+    have /join_symmetric {}h : join A A0 by hauto lq:on ctrs:rtc use:RPar'_Par, relations.rtc_once.
     eauto using join_transitive.
 Qed.
 
-Lemma InterpUniv_Join i (A B : Tm 0) PA PB :
+Lemma InterpUniv_Join n i (A B : Tm n) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ B ⟧ i ↘ PB ->
   join A B ->
   PA = PB.
 Proof. hauto l:on use:InterpExt_Join rew:db:InterpUniv. Qed.
 
-Lemma InterpUniv_Bind_inv p i  (A : Tm 0) B P
+Lemma InterpUniv_Bind_inv n p i  (A : Tm n) B P
   (h :  ⟦ TBind p A B ⟧ i ↘ P) :
-  exists (PA : Tm 0 -> Prop) (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop),
+  exists (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop),
      ⟦ A ⟧ i ↘ PA /\
     (forall a, PA a -> exists PB, PF a PB) /\
     (forall a PB, PF a PB -> ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) /\
     P = BindSpace p PA PF.
 Proof. hauto l:on use:InterpExt_Bind_inv rew:db:InterpUniv. Qed.
 
-Lemma InterpUniv_Univ_inv i j P
+Lemma InterpUniv_Univ_inv n i j P
   (h :  ⟦ Univ j  ⟧ i ↘ P) :
-  P = (fun (A : Tm 0) => exists PA, ⟦ A ⟧ j ↘ PA) /\ j < i.
+  P = (fun (A : Tm n) => exists PA, ⟦ A ⟧ j ↘ PA) /\ j < i.
 Proof. hauto l:on use:InterpExt_Univ_inv rew:db:InterpUniv. Qed.
 
-Lemma InterpExt_Functional i I (A B : Tm 0) PA PB :
+Lemma InterpExt_Functional n i I (A B : Tm n) PA PB :
   ⟦ A ⟧ i ;; I ↘ PA ->
   ⟦ A ⟧ i ;; I ↘ PB ->
   PA = PB.
 Proof. hauto use:InterpExt_Join, join_refl. Qed.
 
-Lemma InterpUniv_Functional i (A : Tm 0) PA PB :
+Lemma InterpUniv_Functional n i (A : Tm n) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ A ⟧ i ↘ PB ->
   PA = PB.
 Proof. hauto use:InterpExt_Functional rew:db:InterpUniv. Qed.
 
-Lemma InterpUniv_Join' i j (A B : Tm 0) PA PB :
+Lemma InterpUniv_Join' n i j (A B : Tm n) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ B ⟧ j ↘ PB ->
   join A B ->
@@ -335,16 +439,16 @@ Proof.
   eauto using InterpUniv_Join.
 Qed.
 
-Lemma InterpUniv_Functional' i j A PA PB :
-  ⟦ A ⟧ i ↘ PA ->
+Lemma InterpUniv_Functional' n i j A PA PB :
+  ⟦ A : Tm n ⟧ i ↘ PA ->
   ⟦ A ⟧ j ↘ PB ->
   PA = PB.
 Proof.
   hauto l:on use:InterpUniv_Join', join_refl.
 Qed.
 
-Lemma InterpExt_Bind_inv_nopf i I p A B P (h :  ⟦TBind p A B ⟧ i ;; I ↘ P) :
-  exists (PA : Tm 0 -> Prop),
+Lemma InterpExt_Bind_inv_nopf i n I p A B P (h :  ⟦TBind p A B ⟧ i ;; I ↘ P) :
+  exists (PA : Tm n -> Prop),
      ⟦ A ⟧ i ;; I ↘ PA /\
     (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) /\
       P = BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB).
@@ -365,34 +469,42 @@ Proof.
       split; hauto q:on use:InterpExt_Functional.
 Qed.
 
-Lemma InterpUniv_Bind_inv_nopf i p A B P (h :  ⟦TBind p A B ⟧ i ↘ P) :
-  exists (PA : Tm 0 -> Prop),
+Lemma InterpUniv_Bind_inv_nopf n i p A B P (h :  ⟦TBind p A B ⟧ i ↘ P) :
+  exists (PA : Tm n -> Prop),
      ⟦ A ⟧ i ↘ PA /\
     (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) /\
       P = BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB).
 Proof. hauto l:on use:InterpExt_Bind_inv_nopf rew:db:InterpUniv. Qed.
 
-Lemma InterpExt_back_clos i I (A : Tm 0) PA :
-  (forall j,  forall a b, (RPar.R a b) ->  I j b -> I j a) ->
+Lemma InterpExt_back_clos n i I (A : Tm n) PA :
+  (forall j,  j < i -> forall a b, (RPar'.R a b) ->  I j b -> I j a) ->
     ⟦ A ⟧ i ;; I ↘ PA ->
-    forall a b, (RPar.R a b) ->
+    forall a b, (RPar'.R a b) ->
            PA b -> PA a.
 Proof.
   move => hI h.
   elim : A PA /h.
+  - hauto q:on ctrs:rtc unfold:wne.
   - move => p A B PA PF hPA ihPA hTot hRes ihPF a b hr.
     case : p => //=.
-    + have  : forall b0 b1 a, RPar.R b0 b1 -> RPar.R (App b0 a) (App b1 a)
-          by hauto lq:on ctrs:RPar.R use:RPar.refl.
+    + have  : forall b0 b1 a, RPar'.R b0 b1 -> RPar'.R (App b0 a) (App b1 a)
+          by hauto lq:on ctrs:RPar'.R use:RPar'.refl.
       hauto lq:on rew:off unfold:ProdSpace.
     + hauto lq:on ctrs:rtc unfold:SumSpace.
   - eauto.
   - eauto.
 Qed.
 
-Lemma InterpUniv_back_clos i (A : Tm 0) PA :
+Lemma InterpExt_back_clos_star n i I (A : Tm n) PA :
+  (forall j,  j < i -> forall a b, (RPar'.R a b) ->  I j b -> I j a) ->
+    ⟦ A ⟧ i ;; I ↘ PA ->
+    forall a b, (rtc RPar'.R a b) ->
+           PA b -> PA a.
+Proof. induction 3; hauto l:on use:InterpExt_back_clos. Qed.
+
+Lemma InterpUniv_back_clos n i (A : Tm n) PA :
     ⟦ A ⟧ i ↘ PA ->
-    forall a b, (RPar.R a b) ->
+    forall a b, (RPar'.R a b) ->
            PA b -> PA a.
 Proof.
   simp InterpUniv.
@@ -400,9 +512,9 @@ Proof.
   hauto lq:on ctrs:rtc use:InterpUnivN_back_preservation_star.
 Qed.
 
-Lemma InterpUniv_back_clos_star i (A : Tm 0) PA :
+Lemma InterpUniv_back_clos_star n i (A : Tm n) PA :
     ⟦ A ⟧ i ↘ PA ->
-    forall a b, rtc RPar.R a b ->
+    forall a b, rtc RPar'.R a b ->
            PA b -> PA a.
 Proof.
   move => h  a b.
@@ -410,30 +522,101 @@ Proof.
   hauto lq:on use:InterpUniv_back_clos.
 Qed.
 
-Definition ρ_ok {n} Γ (ρ : fin n -> Tm 0) := forall i m PA,
-  ⟦ subst_Tm ρ (Γ i) ⟧ m ↘ PA -> PA (ρ i).
+Lemma pars'_wn {n} a b :
+  rtc RPar'.R a b ->
+  @wn n b ->
+  wn a.
+Proof. sfirstorder unfold:wn use:@relations.rtc_transitive. Qed.
 
-Definition SemWt {n} Γ (a A : Tm n) := forall ρ, ρ_ok Γ ρ -> exists m PA, ⟦ subst_Tm ρ A ⟧ m ↘ PA /\ PA (subst_Tm ρ a).
+(* P identifies a set of "reducibility candidates" *)
+Definition CR {n} (P : Tm n -> Prop) :=
+  (forall a, P a -> wn a) /\
+    (forall a, ne a -> P a).
+
+Lemma adequacy_ext i n I A PA
+  (hI0 : forall j,  j < i -> forall a b, (RPar'.R a b) ->  I j b -> I j a)
+  (hI : forall j, j < i -> CR (I j))
+  (h :  ⟦ A : Tm n ⟧ i ;; I ↘ PA) :
+  CR PA /\ wn A.
+Proof.
+  elim : A PA / h.
+  - hauto unfold:wne use:wne_wn.
+  - move => p A B PA PF hA hPA hTot hRes ihPF.
+    rewrite /CR.
+    have hb : PA Bot by firstorder.
+    repeat split.
+    + case : p => /=.
+      * qauto l:on use:ext_wn unfold:ProdSpace, CR.
+      * rewrite /SumSpace => a []; first by eauto with nfne.
+        move => [q0][q1]*.
+        have : wn q0 /\ wn q1 by hauto q:on.
+        qauto l:on use:wn_pair, pars'_wn.
+    + case : p => /=.
+      * rewrite /ProdSpace.
+        move => a ha c PB hc hPB.
+        have hc' : wn c by sfirstorder.
+        have : wne (App a c) by hauto lq:on use:wne_app ctrs:rtc.
+        have h : (forall a, ne a -> PB a) by sfirstorder.
+        suff : (forall a, wne a -> PB a) by hauto l:on.
+        move => a0 [a1 [h0 h1]].
+        eapply InterpExt_back_clos_star with (b := a1); eauto.
+      * rewrite /SumSpace.
+        move => a ha. left.
+        sfirstorder ctrs:rtc.
+    + have wnA : wn A by firstorder.
+      apply wn_bind => //.
+      apply wn_antirenaming with (ρ := scons Bot VarTm);first by  hauto q:on inv:option.
+      hauto lq:on.
+  - hauto l:on.
+  - hauto lq:on rew:off ctrs:rtc.
+Qed.
+
+Lemma adequacy i n A PA
+  (h :  ⟦ A : Tm n ⟧ i ↘ PA) :
+  CR PA /\ wn A.
+Proof.
+  move : i A PA h.
+  elim /Wf_nat.lt_wf_ind => i ih A PA.
+  simp InterpUniv.
+  apply adequacy_ext.
+  hauto lq:on ctrs:rtc use:InterpUnivN_back_preservation_star.
+  hauto l:on use:InterpExt_Ne rew:db:InterpUniv.
+Qed.
+
+Lemma adequacy_wne i n A PA a : ⟦ A : Tm n ⟧ i ↘ PA -> wne a -> PA a.
+Proof. qauto l:on use:InterpUniv_back_clos_star, adequacy unfold:CR. Qed.
+
+Lemma adequacy_wn i n A PA (h :  ⟦ A : Tm n ⟧ i ↘ PA) a : PA a -> wn a.
+Proof. hauto q:on use:adequacy. Qed.
+
+Definition ρ_ok {n} (Γ : fin n -> Tm n) (ρ : fin n -> Tm 0) := forall i k PA,
+  ⟦ subst_Tm ρ (Γ i) ⟧ k ↘ PA -> PA (ρ i).
+
+Definition SemWt {n} Γ (a A : Tm n) := forall ρ, ρ_ok Γ ρ -> exists k PA, ⟦ subst_Tm ρ A ⟧ k ↘ PA /\ PA (subst_Tm ρ a).
 Notation "Γ ⊨ a ∈ A" := (SemWt Γ a A) (at level 70).
 
 (* Semantic context wellformedness *)
 Definition SemWff {n} Γ := forall (i : fin n), exists j, Γ ⊨ Γ i ∈ Univ j.
 Notation "⊨ Γ" := (SemWff Γ) (at level 70).
 
-Lemma ρ_ok_nil ρ :
-  ρ_ok null ρ.
-Proof.  rewrite /ρ_ok. inversion i; subst. Qed.
+Lemma ρ_ok_bot n (Γ : fin n -> Tm n)  :
+  ρ_ok Γ (fun _ => Bot).
+Proof.
+  rewrite /ρ_ok.
+  hauto q:on use:adequacy.
+Qed.
 
 Lemma ρ_ok_cons n i (Γ : fin n -> Tm n) ρ a PA A :
   ⟦ subst_Tm ρ A ⟧ i ↘ PA -> PA a ->
   ρ_ok Γ ρ ->
-  ρ_ok (funcomp (ren_Tm shift) (scons A Γ)) ((scons a ρ)).
+  ρ_ok (funcomp (ren_Tm shift) (scons A Γ)) (scons a ρ).
 Proof.
   move => h0 h1 h2.
   rewrite /ρ_ok.
   move => j.
   destruct j as [j|].
   - move => m PA0. asimpl => ?.
+    asimpl.
     firstorder.
   - move => m PA0. asimpl => h3.
     have ? : PA0 = PA by eauto using InterpUniv_Functional'.
@@ -455,7 +638,7 @@ Proof.
   rewrite /ρ_ok in hρ.
   move => h.
   rewrite /funcomp.
-  apply hρ with (m := m').
+  apply hρ with (k := m').
   move : h. rewrite -hξ.
   by asimpl.
 Qed.
@@ -480,6 +663,17 @@ Proof.
   hauto lq:on inv:option unfold:renaming_ok.
 Qed.
 
+Lemma SemWt_Wn n Γ (a : Tm n) A :
+  Γ ⊨ a ∈ A ->
+  wn a /\ wn A.
+Proof.
+  move => h.
+  have {}/h := ρ_ok_bot _ Γ => h.
+  have h0 : wn (subst_Tm (fun _ : fin n => (Bot : Tm 0)) A) by hauto l:on use:adequacy.
+  have h1 : wn (subst_Tm (fun _ : fin n => (Bot : Tm 0)) a)by hauto l:on use:adequacy_wn.
+  move {h}. hauto lq:on use:wn_antirenaming.
+Qed.
+
 Lemma SemWt_Univ n Γ (A : Tm n) i  :
   Γ ⊨ A ∈ Univ i <->
   forall ρ, ρ_ok Γ ρ -> exists S, ⟦ subst_Tm ρ A ⟧ i ↘ S.
@@ -572,7 +766,7 @@ Proof.
   intros (m & PB0 & hPB0 & hPB0').
   replace PB0 with PB in * by hauto l:on use:InterpUniv_Functional'.
   apply : InterpUniv_back_clos; eauto.
-  apply : RPar.AppAbs'; eauto using RPar.refl.
+  apply : RPar'.AppAbs'; eauto using RPar'.refl.
   by asimpl.
 Qed.
 
@@ -604,7 +798,7 @@ Proof.
   simpl in hPPi.
   move /InterpUniv_Bind_inv_nopf : hPPi.
   move => [PA [hPA [hTot ?]]]. subst=>/=.
-  rewrite /SumSpace.
+  rewrite /SumSpace. right.
   exists (subst_Tm ρ a), (subst_Tm ρ b).
   split.
   - hauto l:on use:Pars.substing.
@@ -626,24 +820,25 @@ Proof.
   move : h0 => [S][h2][h3]?. subst.
   move : h1 => /=.
   rewrite /SumSpace.
+  case; first by hauto lq:on use:adequacy_wne, wne_proj.
   move => [a0 [b0 [h4 [h5 h6]]]].
   exists m, S. split => //=.
-  have {}h4 : rtc RPar.R (Proj PL (subst_Tm ρ a)) (Proj PL (Pair a0 b0)) by eauto using RPars.ProjCong.
-  have ? : RPar.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar.refl, RPar.ProjPair'.
-  have : rtc RPar.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
+  have {}h4 : rtc RPar'.R (Proj PL (subst_Tm ρ a)) (Proj PL (Pair a0 b0)) by eauto using RPars'.ProjCong.
+  have ? : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.refl, RPar'.ProjPair'.
+  have : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
   move => h.
   apply : InterpUniv_back_clos_star; eauto.
 Qed.
 
-Lemma substing_RPar n m (A : Tm (S n)) ρ (B : Tm m) C :
-  RPar.R B C ->
-  RPar.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
-Proof. hauto lq:on inv:option use:RPar.morphing, RPar.refl. Qed.
+Lemma substing_RPar' n m (A : Tm (S n)) ρ (B : Tm m) C :
+  RPar'.R B C ->
+  RPar'.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
+Proof. hauto lq:on inv:option use:RPar'.morphing, RPar'.refl. Qed.
 
-Lemma substing_RPars n m (A : Tm (S n)) ρ (B : Tm m) C :
-  rtc RPar.R B C ->
-  rtc RPar.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
-Proof. induction 1; hauto lq:on ctrs:rtc use:substing_RPar. Qed.
+Lemma substing_RPar's n m (A : Tm (S n)) ρ (B : Tm m) C :
+  rtc RPar'.R B C ->
+  rtc RPar'.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
+Proof. induction 1; hauto lq:on ctrs:rtc use:substing_RPar'. Qed.
 
 Lemma ST_Proj2 n Γ (a : Tm n) A B :
   Γ ⊨ a ∈ TBind TSig A B ->
@@ -654,17 +849,155 @@ Proof.
   move : h0 => [S][h2][h3]?. subst.
   move : h1 => /=.
   rewrite /SumSpace.
-  move => [a0 [b0 [h4 [h5 h6]]]].
-  specialize h3 with (1 := h5).
-  move : h3 => [PB hPB].
-  have hr : forall p, rtc RPar.R (Proj p (subst_Tm ρ a)) (Proj p (Pair a0 b0)) by eauto using RPars.ProjCong.
-  have hrl : RPar.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar.ProjPair', RPar.refl.
-  have hrr : RPar.R (Proj PR (Pair a0 b0)) b0 by hauto l:on use:RPar.ProjPair', RPar.refl.
-  exists m, PB.
-  asimpl. split.
-  - have h : rtc RPar.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
-    have {}h : rtc RPar.R (subst_Tm (scons (Proj PL (subst_Tm ρ a)) ρ) B) (subst_Tm (scons a0 ρ) B) by eauto using substing_RPars.
-    move : hPB. asimpl.
-    eauto using InterpUnivN_back_preservation_star.
-  - hauto lq:on use:@relations.rtc_r, InterpUniv_back_clos_star.
+  case.
+  - move => h.
+    have hp : forall p, wne (Proj p (subst_Tm ρ a)) by auto using wne_proj.
+    have hp0 := hp PL. have hp1 := hp PR => {hp}.
+    have : S (Proj PL (subst_Tm ρ a)) by hauto q:on use:adequacy_wne.
+    move /h3 => [PB]. asimpl. hauto lq:on use:adequacy_wne.
+  - move => [a0 [b0 [h4 [h5 h6]]]].
+    specialize h3 with (1 := h5).
+    move : h3 => [PB hPB].
+    have hr : forall p, rtc RPar'.R (Proj p (subst_Tm ρ a)) (Proj p (Pair a0 b0)) by eauto using RPars'.ProjCong.
+    have hrl : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.ProjPair', RPar'.refl.
+    have hrr : RPar'.R (Proj PR (Pair a0 b0)) b0 by hauto l:on use:RPar'.ProjPair', RPar'.refl.
+    exists m, PB.
+    asimpl. split.
+    + have h : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
+      have {}h : rtc RPar'.R (subst_Tm (scons (Proj PL (subst_Tm ρ a)) ρ) B) (subst_Tm (scons a0 ρ) B) by eauto using substing_RPar's.
+      move : hPB. asimpl.
+      eauto using InterpUnivN_back_preservation_star.
+    + hauto lq:on use:@relations.rtc_r, InterpUniv_back_clos_star.
 Qed.
+
+Lemma ne_nf_preservation n (a b : Tm n) : ERed.R b a -> (ne a -> ne b) /\ (nf a -> nf b).
+Proof.
+  move => h. elim : n b a /h => //=.
+  - move => n a.
+    split => //=.
+    hauto lqb:on use:ne_nf_ren db:nfne.
+  - hauto lqb:on db:nfne.
+  - hauto lqb:on db:nfne.
+  - hauto lqb:on db:nfne.
+  - hauto lqb:on db:nfne.
+  - hauto lqb:on db:nfne.
+  - hauto lqb:on db:nfne.
+  - hauto lqb:on db:nfne.
+  - hauto lqb:on db:nfne.
+  - hauto lqb:on db:nfne.
+Qed.
+
+Fixpoint size_tm {n} (a : Tm n) :=
+  match a with
+  | VarTm _ => 1
+  | TBind _ A B => 1 + Nat.add (size_tm A) (size_tm B)
+  | Abs a => 1 + size_tm a
+  | App a b => 1 + Nat.add (size_tm a) (size_tm b)
+  | Proj p a => 1 + size_tm a
+  | Pair a b => 1 + Nat.add (size_tm a) (size_tm b)
+  | Bot => 1
+  | Univ _ => 1
+  end.
+
+Lemma size_tm_ren n m (ξ : fin n -> fin m) a : size_tm (ren_Tm ξ a) = size_tm a.
+Proof.
+  move : m ξ. elim : n / a => //=; scongruence.
+Qed.
+
+#[export]Hint Rewrite size_tm_ren : size_tm.
+
+Lemma size_η_lt n (a b : Tm n) :
+  ERed.R b a ->
+  size_tm b < size_tm a.
+Proof.
+  move => h. elim : b a / h => //=; hauto l:on rew:db:size_tm.
+Qed.
+
+Lemma ered_local_confluence n (a b c : Tm n) :
+  ERed.R b a ->
+  ERed.R c a ->
+  exists d, rtc ERed.R d b  /\ rtc ERed.R d c.
+Proof.
+  move => h. move : c.
+  elim : n b a / h => n.
+  - move => a c.
+    elim /ERed.inv => //= _.
+    + move => ? ? [*]. subst.
+      have : subst_Tm (scons Bot VarTm) (ren_Tm shift c) = (subst_Tm (scons Bot VarTm) (ren_Tm shift a))
+        by congruence.
+      asimpl => ?. subst.
+      eauto using rtc_refl.
+    + move => a0 a1 ha ? [*]. subst.
+      elim /ERed.inv : ha => //= _.
+      * move => a1 a2 b0 ha ? [*]. subst.
+        have [a2 [h0 h1]] : exists a2, ERed.R a2 a /\ a1 = ren_Tm shift a2 by admit. subst.
+        eexists. split; cycle 1.
+        apply : relations.rtc_r; cycle 1.
+        apply ERed.AppEta.
+        apply rtc_refl.
+        eauto using relations.rtc_once.
+      * hauto q:on ctrs:rtc, ERed.R inv:ERed.R.
+  - move => a c ha.
+    elim /ERed.inv : ha => //= _.
+    + hauto l:on.
+    + move => a0 a1 b0 ha ? [*]. subst.
+      elim /ERed.inv : ha => //= _.
+      move => p a1 a2 ha ? [*]. subst.
+      exists a1. split. by apply relations.rtc_once.
+      apply : rtc_l. apply ERed.PairEta.
+      apply : rtc_l. apply ERed.PairCong1. eauto using ERed.ProjCong.
+      apply rtc_refl.
+    + move => a0 b0 b1 ha ? [*]. subst.
+      elim /ERed.inv : ha => //= _ p a0 a1 h ? [*]. subst.
+      exists a0. split; first by apply relations.rtc_once.
+      apply : rtc_l; first by apply ERed.PairEta.
+      apply relations.rtc_once.
+      hauto lq:on ctrs:ERed.R.
+  - move => a0 a1 ha iha c.
+    elim /ERed.inv => //= _.
+    + move => a2 ? [*]. subst.
+      elim /ERed.inv : ha => //=_.
+      * move => a1 a2 b0 ha ? [*] {iha}. subst.
+        have [a0 [h0 h1]] : exists a0, ERed.R a0 c /\ a1 = ren_Tm shift a0 by admit. subst.
+        exists a0. split; last by apply relations.rtc_once.
+        apply relations.rtc_once. apply ERed.AppEta.
+      * hauto q:on inv:ERed.R.
+    + hauto l:on use:EReds.AbsCong.
+  - move => a0 a1 b ha iha c.
+    elim /ERed.inv => //= _.
+    + hauto lq:on ctrs:rtc use:EReds.AppCong.
+    + hauto lq:on use:@relations.rtc_once ctrs:ERed.R.
+  - move => a b0 b1 hb ihb c.
+    elim /ERed.inv => //=_.
+    + move => a0 a1 a2 ha ? [*]. subst.
+      move {ihb}. exists (App a0 b0).
+      hauto lq:on use:@relations.rtc_once ctrs:ERed.R.
+    + hauto lq:on ctrs:rtc use:EReds.AppCong.
+  - move => a0 a1 b ha iha c.
+    elim /ERed.inv => //= _.
+    + move => ? ?[*]. subst.
+      elim /ERed.inv : ha => //= _ p a1 a2 h ? [*]. subst.
+      exists a1. split; last by apply relations.rtc_once.
+      apply : rtc_l. apply ERed.PairEta.
+      apply relations.rtc_once. hauto lq:on ctrs:ERed.R.
+    + hauto lq:on ctrs:rtc use:EReds.PairCong.
+    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
+  - move => a b0 b1 hb hc c. elim /ERed.inv => //= _.
+    + move => ? ? [*]. subst.
+      elim /ERed.inv : hb => //= _ p a0 a1 ha ? [*]. subst.
+      move {hc}.
+      exists a0. split; last by apply relations.rtc_once.
+      apply : rtc_l; first by apply ERed.PairEta.
+      hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
+    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
+    + hauto lq:on ctrs:rtc use:EReds.PairCong.
+  - qauto l:on inv:ERed.R use:EReds.ProjCong.
+  - move => p A0 A1 B hA ihA.
+    move => c. elim/ERed.inv => //=.
+    + hauto lq:on ctrs:rtc use:EReds.BindCong.
+    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
+  - move => p A B0 B1 hB ihB c.
+    elim /ERed.inv => //=.
+    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
+    + hauto lq:on ctrs:rtc use:EReds.BindCong.
+Admitted.