diff --git a/theories/algorithmic.v b/theories/algorithmic.v
index 3046ced..444f49f 100644
--- a/theories/algorithmic.v
+++ b/theories/algorithmic.v
@@ -1,10 +1,11 @@
 Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax
-  common typing preservation admissible fp_red structural.
+  common typing preservation admissible fp_red structural soundness.
 From Hammer Require Import Tactics.
 Require Import ssreflect ssrbool.
 Require Import Psatz.
-From stdpp Require Import relations (rtc(..)).
+From stdpp Require Import relations (rtc(..), nsteps(..)).
 Require Import Coq.Logic.FunctionalExtensionality.
+Require Import Cdcl.Itauto.
 
 Module HRed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
@@ -58,6 +59,169 @@ Lemma E_Conv_E n Γ (a b : PTm n) A B i :
   Γ ⊢ a ≡ b ∈ B.
 Proof. qauto use:E_Conv, Su_Eq, E_Symmetric. Qed.
 
+Lemma lored_embed n Γ (a b : PTm n) A :
+  Γ ⊢ a ∈ A -> LoRed.R a b -> Γ ⊢ a ≡ b ∈ A.
+Proof. sfirstorder use:LoRed.ToRRed, RRed_Eq. Qed.
+
+Lemma loreds_embed n Γ (a b : PTm n) A :
+  Γ ⊢ a ∈ A -> rtc LoRed.R a b -> Γ ⊢ a ≡ b ∈ A.
+Proof.
+  move => + h. move : Γ A.
+  elim : a b /h.
+  - sfirstorder use:E_Refl.
+  - move => a b c ha hb ih Γ A hA.
+    have ? : Γ ⊢ a ≡ b ∈ A by sfirstorder use:lored_embed.
+    have ? : Γ ⊢ b ∈ A by hauto l:on use:regularity.
+    hauto lq:on ctrs:Eq.
+Qed.
+
+Lemma T_Bot_Imp n Γ (A : PTm n) :
+  Γ ⊢ PBot ∈ A -> False.
+  move E : PBot => u hu.
+  move : E.
+  induction hu => //=.
+Qed.
+
+Lemma Sub_Bind_InvR n Γ p (A : PTm n) B C :
+  Γ ⊢ PBind p A B ≲ C ->
+  exists i A0 B0, Γ ⊢ C ≡ PBind p A0 B0 ∈ PUniv i.
+Proof.
+  move => /[dup] h.
+  move /synsub_to_usub.
+  move => [h0 [h1 h2]].
+  move /LoReds.FromSN : h1.
+  move => [C' [hC0 hC1]].
+  have [i hC] : exists i, Γ ⊢ C ∈ PUniv i by qauto l:on use:regularity.
+  have hE : Γ ⊢ C ≡ C' ∈ PUniv i by sfirstorder use:loreds_embed.
+  have : Γ ⊢ PBind p A B ≲ C' by eauto using Su_Transitive, Su_Eq.
+  move : hE hC1. clear.
+  case : C' => //=.
+  - move => k _ _ /synsub_to_usub.
+    clear. move => [_ [_ h]]. exfalso.
+    rewrite /Sub.R in h.
+    move : h => [c][d][+ []].
+    move /REReds.bind_inv => ?.
+    move /REReds.var_inv => ?.
+    sauto lq:on.
+  - move => p0 h. exfalso.
+    have {h} : Γ ⊢ PAbs p0 ∈ PUniv i by hauto l:on use:regularity.
+    move /Abs_Inv => [A0][B0][_]/synsub_to_usub.
+    hauto l:on use:Sub.bind_univ_noconf.
+  - move => u v hC /andP [h0 h1] /synsub_to_usub ?.
+    exfalso.
+    suff : SNe (PApp u v) by hauto l:on use:Sub.bind_sne_noconf.
+    eapply ne_nf_embed => //=. itauto.
+  - move => p0 p1 hC  h  ?. exfalso.
+    have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity.
+    hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv.
+  - move => p0 p1 _ + /synsub_to_usub.
+    hauto lq:on use:Sub.bind_sne_noconf, ne_nf_embed.
+  - move => b p0 p1 h0 h1 /[dup] h2 /synsub_to_usub *.
+    have ? : b = p by hauto l:on use:Sub.bind_inj. subst.
+    eauto.
+  - hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf.
+  - hauto lq:on use:regularity, T_Bot_Imp.
+Qed.
+
+Lemma Sub_Univ_InvR n (Γ : fin n -> PTm n) i C :
+  Γ ⊢ PUniv i ≲ C ->
+  exists j k, Γ ⊢ C ≡ PUniv j ∈ PUniv k.
+Proof.
+  move => /[dup] h.
+  move /synsub_to_usub.
+  move => [h0 [h1 h2]].
+  move /LoReds.FromSN : h1.
+  move => [C' [hC0 hC1]].
+  have [j hC] : exists i, Γ ⊢ C ∈ PUniv i by qauto l:on use:regularity.
+  have hE : Γ ⊢ C ≡ C' ∈ PUniv j by sfirstorder use:loreds_embed.
+  have : Γ ⊢ PUniv i ≲ C' by eauto using Su_Transitive, Su_Eq.
+  move : hE hC1. clear.
+  case : C' => //=.
+  - move => f => _ _ /synsub_to_usub.
+    move => [_ [_]].
+    move => [v0][v1][/REReds.univ_inv + [/REReds.var_inv ]].
+    hauto lq:on inv:Sub1.R.
+  - move => p hC.
+    have {hC} : Γ ⊢ PAbs p ∈ PUniv j by hauto l:on use:regularity.
+    hauto lq:on rew:off use:Abs_Inv, synsub_to_usub,
+            Sub.bind_univ_noconf.
+  - hauto q:on use:synsub_to_usub, Sub.univ_sne_noconf, ne_nf_embed.
+  - move => a b hC.
+    have {hC} : Γ ⊢ PPair a b ∈ PUniv j by hauto l:on use:regularity.
+    hauto lq:on rew:off use:Pair_Inv, synsub_to_usub,
+            Sub.bind_univ_noconf.
+  - hauto q:on use:synsub_to_usub, Sub.univ_sne_noconf, ne_nf_embed.
+  - hauto lq:on use:synsub_to_usub, Sub.univ_bind_noconf.
+  - sfirstorder.
+  - hauto lq:on use:regularity, T_Bot_Imp.
+Qed.
+
+Lemma Sub_Bind_InvL n Γ p (A : PTm n) B C :
+  Γ ⊢ C ≲ PBind p A B ->
+  exists i A0 B0, Γ ⊢ PBind p A0 B0 ≡ C ∈ PUniv i.
+Proof.
+  move => /[dup] h.
+  move /synsub_to_usub.
+  move => [h0 [h1 h2]].
+  move /LoReds.FromSN : h0.
+  move => [C' [hC0 hC1]].
+  have [i hC] : exists i, Γ ⊢ C ∈ PUniv i by qauto l:on use:regularity.
+  have hE : Γ ⊢ C ≡ C' ∈ PUniv i by sfirstorder use:loreds_embed.
+  have : Γ ⊢ C' ≲ PBind p A B by eauto using Su_Transitive, Su_Eq, E_Symmetric.
+  move : hE hC1. clear.
+  case : C' => //=.
+  - move => k _ _ /synsub_to_usub.
+    clear. move => [_ [_ h]]. exfalso.
+    rewrite /Sub.R in h.
+    move : h => [c][d][+ []].
+    move /REReds.var_inv => ?.
+    move /REReds.bind_inv => ?.
+    hauto lq:on inv:Sub1.R.
+  - move => p0 h. exfalso.
+    have {h} : Γ ⊢ PAbs p0 ∈ PUniv i by hauto l:on use:regularity.
+    move /Abs_Inv => [A0][B0][_]/synsub_to_usub.
+    hauto l:on use:Sub.bind_univ_noconf.
+  - move => u v hC /andP [h0 h1] /synsub_to_usub ?.
+    exfalso.
+    suff : SNe (PApp u v) by hauto l:on use:Sub.sne_bind_noconf.
+    eapply ne_nf_embed => //=. itauto.
+  - move => p0 p1 hC  h  ?. exfalso.
+    have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity.
+    hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv.
+  - move => p0 p1 _ + /synsub_to_usub.
+    hauto lq:on use:Sub.sne_bind_noconf, ne_nf_embed.
+  - move => b p0 p1 h0 h1 /[dup] h2 /synsub_to_usub *.
+    have ? : b = p by hauto l:on use:Sub.bind_inj. subst.
+    eauto using E_Symmetric.
+  - hauto lq:on use:synsub_to_usub, Sub.univ_bind_noconf.
+  - hauto lq:on use:regularity, T_Bot_Imp.
+Qed.
+
+Lemma T_Abs_Inv n Γ (a0 a1 : PTm (S n)) U :
+  Γ ⊢ PAbs a0 ∈ U ->
+  Γ ⊢ PAbs a1 ∈ U ->
+  exists Δ V, Δ ⊢ a0 ∈ V /\ Δ ⊢ a1 ∈ V.
+Proof.
+  move /Abs_Inv => [A0][B0][wt0]hU0.
+  move /Abs_Inv => [A1][B1][wt1]hU1.
+  move /Sub_Bind_InvR : (hU0) => [i][A2][B2]hE.
+  have hSu : Γ ⊢ PBind PPi A1 B1 ≲ PBind PPi A2 B2 by eauto using Su_Eq, Su_Transitive.
+  have hSu' : Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A2 B2 by eauto using Su_Eq, Su_Transitive.
+  exists (funcomp (ren_PTm shift) (scons A2 Γ)), B2.
+  have [k ?] : exists k, Γ ⊢ A2 ∈ PUniv k by hauto lq:on use:regularity, Bind_Inv.
+  split.
+  - have /Su_Pi_Proj2_Var ? := hSu'.
+    have /Su_Pi_Proj1 ? := hSu'.
+    move /regularity_sub0 : hSu' => [j] /Bind_Inv [k0 [? ?]].
+    apply T_Conv with (A := B0); eauto.
+    apply : ctx_eq_subst_one; eauto.
+  - have /Su_Pi_Proj2_Var ? := hSu.
+    have /Su_Pi_Proj1 ? := hSu.
+    move /regularity_sub0 : hSu => [j] /Bind_Inv [k0 [? ?]].
+    apply T_Conv with (A := B1); eauto.
+    apply : ctx_eq_subst_one; eauto.
+Qed.
+
 (* Coquand's algorithm with subtyping *)
 Reserved Notation "a ∼ b" (at level 70).
 Reserved Notation "a ↔ b" (at level 70).
@@ -145,6 +309,14 @@ with CoqEq_R {n} : PTm n -> PTm n -> Prop :=
   a ⇔ b
 where "a ↔ b" := (CoqEq a b) and "a ⇔ b" := (CoqEq_R a b) and "a ∼ b" := (CoqEq_Neu a b).
 
+Lemma CE_HRedL n (a a' b : PTm n)  :
+  HRed.R a a' ->
+  a' ⇔ b ->
+  a ⇔ b.
+Proof.
+  hauto lq:on ctrs:rtc, CoqEq_R inv:CoqEq_R.
+Qed.
+
 Scheme
   coqeq_neu_ind := Induction for CoqEq_Neu Sort Prop
   with coqeq_ind := Induction for CoqEq Sort Prop
@@ -158,23 +330,6 @@ Lemma coqeq_symmetric_mutual : forall n,
     (forall (a b : PTm n), a ⇔ b -> b ⇔ a).
 Proof. apply coqeq_mutual; qauto l:on ctrs:CoqEq,CoqEq_R, CoqEq_Neu. Qed.
 
-Lemma Sub_Bind_InvR n Γ p (A : PTm n) B C :
-  Γ ⊢ PBind p A B ≲ C ->
-  exists i A0 B0, Γ ⊢ C ≡ PBind p A0 B0 ∈ PUniv i.
-Proof.
-Admitted.
-
-Lemma Sub_Bind_InvL n Γ p (A : PTm n) B C :
-  Γ ⊢ C ≲ PBind p A B ->
-  exists i A0 B0, Γ ⊢ PBind p A0 B0 ≡ C ∈ PUniv i.
-Proof.
-Admitted.
-
-Lemma Sub_Univ_InvR n (Γ : fin n -> PTm n) i C :
-  Γ ⊢ PUniv i ≲ C ->
-  exists j, Γ ⊢ C ≡ PUniv j ∈ PUniv (S j).
-Proof.
-Admitted.
 
 (* Lemma Sub_Univ_InvR *)
 
@@ -384,3 +539,810 @@ Proof.
     have [*] : Γ ⊢ a' ∈ A /\ Γ ⊢ b' ∈ A by eauto using HReds.preservation.
     hauto lq:on use:HReds.ToEq, E_Symmetric, E_Transitive.
 Qed.
+
+Definition algo_metric {n} k (a b : PTm n) :=
+  exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ EJoin.R va vb /\ size_PTm va + size_PTm vb + i + j <= k.
+
+Lemma ne_hne n (a : PTm n) : ne a -> ishne a.
+Proof. elim : a => //=; sfirstorder b:on. Qed.
+
+Lemma hf_hred_lored n (a b : PTm n) :
+  ~~ ishf a ->
+  LoRed.R a b ->
+  HRed.R a b \/ ishne a.
+Proof.
+  move => + h. elim : n a b/ h=>//=.
+  - hauto l:on use:HRed.AppAbs.
+  - hauto l:on use:HRed.ProjPair.
+  - hauto lq:on ctrs:HRed.R.
+  - sfirstorder use:ne_hne.
+  - hauto lq:on ctrs:HRed.R.
+Qed.
+
+Lemma algo_metric_case n k (a b : PTm n) :
+  algo_metric k a b ->
+  (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ algo_metric k' a' b /\ k' < k.
+Proof.
+  move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6.
+  case : a h0 => //=; try firstorder.
+  - inversion h0 as [|A B C D E F]; subst.
+    hauto qb:on use:ne_hne.
+    inversion E; subst => /=.
+    + hauto lq:on use:HRed.AppAbs unfold:algo_metric solve+:lia.
+    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
+    + sfirstorder qb:on use:ne_hne.
+  - inversion h0 as [|A B C D E F]; subst.
+    hauto qb:on use:ne_hne.
+    inversion E; subst => /=.
+    + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia.
+    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
+Qed.
+
+Lemma algo_metric_sym n k (a b : PTm n) :
+  algo_metric k a b -> algo_metric k b a.
+Proof. hauto lq:on unfold:algo_metric solve+:lia. Qed.
+
+Lemma hred_hne n (a b : PTm n) :
+  HRed.R a b ->
+  ishne a ->
+  False.
+Proof. induction 1; sfirstorder. Qed.
+
+Lemma hf_not_hne n (a : PTm n) :
+  ishf a -> ishne a -> False.
+Proof. case : a => //=. Qed.
+
+(* Lemma algo_metric_hf_case n Γ k a b (A : PTm n) : *)
+(*   Γ ⊢ a ∈ A -> *)
+(*   Γ ⊢ b ∈ A -> *)
+(*   algo_metric k a b -> ishf a -> ishf b -> *)
+(*   (exists a' b' k', a = PAbs a' /\ b = PAbs b' /\ algo_metric k' a' b' /\ k' < k) \/ *)
+(*   (exists a0' a1' b0' b1' ka kb, a = PPair a0' a1' /\ b = PPair b0' b1' /\ algo_metric ka a0' b0' /\ algo_metric ) *)
+
+Lemma T_AbsPair_Imp n Γ a (b0 b1 : PTm n) A :
+  Γ ⊢ PAbs a ∈ A ->
+  Γ ⊢ PPair b0 b1 ∈ A ->
+  False.
+Proof.
+  move /Abs_Inv => [A0][B0][_]haU.
+  move /Pair_Inv => [A1][B1][_][_]hbU.
+  move /Sub_Bind_InvR : haU => [i][A2][B2]h2.
+  have : Γ ⊢ PBind PSig A1 B1 ≲ PBind PPi A2 B2 by eauto using Su_Transitive, Su_Eq.
+  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_inj.
+Qed.
+
+Lemma T_PairBind_Imp n Γ (a0 a1 : PTm n) p A0 B0 U :
+  Γ ⊢ PPair a0 a1 ∈ U ->
+  Γ ⊢ PBind p A0 B0  ∈ U ->
+  False.
+Proof.
+  move /Pair_Inv => [A1][B1][_][_]hbU.
+  move /Bind_Inv => [i][_ [_ haU]].
+  move /Sub_Univ_InvR : haU => [j][k]hU.
+  have : Γ ⊢ PBind PSig A1 B1 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
+  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_univ_noconf.
+Qed.
+
+Lemma Univ_Inv n Γ i U :
+  Γ ⊢ @PUniv n i ∈ U ->
+  Γ ⊢ PUniv i ∈ PUniv (S i)  /\ Γ ⊢ PUniv (S i) ≲ U.
+Proof.
+  move E : (PUniv i) => u hu.
+  move : i E. elim : n Γ u U / hu => n //=.
+  - hauto l:on use:E_Refl, Su_Eq, T_Univ.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma T_PairUniv_Imp n Γ (a0 a1 : PTm n) i U :
+  Γ ⊢ PPair a0 a1 ∈ U ->
+  Γ ⊢ PUniv i ∈ U ->
+  False.
+Proof.
+  move /Pair_Inv => [A1][B1][_][_]hbU.
+  move /Univ_Inv => [h0 h1].
+  move /Sub_Univ_InvR : h1 => [j [k hU]].
+  have : Γ ⊢ PBind PSig A1 B1 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
+  clear. move /synsub_to_usub.
+  hauto lq:on use:Sub.bind_univ_noconf.
+Qed.
+
+Lemma T_AbsUniv_Imp n Γ a i (A : PTm n) :
+  Γ ⊢ PAbs a ∈ A ->
+  Γ ⊢ PUniv i ∈ A ->
+  False.
+Proof.
+  move /Abs_Inv => [A0][B0][_]haU.
+  move /Univ_Inv => [h0 h1].
+  move /Sub_Univ_InvR : h1 => [j [k hU]].
+  have : Γ ⊢ PBind PPi A0 B0 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
+  clear. move /synsub_to_usub.
+  hauto lq:on use:Sub.bind_univ_noconf.
+Qed.
+
+Lemma T_AbsBind_Imp n Γ a p A0 B0 (U : PTm n) :
+  Γ ⊢ PAbs a ∈ U ->
+  Γ ⊢ PBind p A0 B0 ∈ U ->
+  False.
+Proof.
+  move /Abs_Inv => [A1][B1][_ ha].
+  move /Bind_Inv => [i [_ [_ h]]].
+  move /Sub_Univ_InvR : h => [j [k hU]].
+  have : Γ ⊢ PBind PPi A1 B1 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
+  clear. move /synsub_to_usub.
+  hauto lq:on use:Sub.bind_univ_noconf.
+Qed.
+
+Lemma lored_nsteps_abs_inv k n (a : PTm (S n)) b :
+  nsteps LoRed.R k (PAbs a) b -> exists b', nsteps LoRed.R k a b' /\ b = PAbs b'.
+Proof.
+  move E : (PAbs a) => u hu.
+  move : a E.
+  elim : u b /hu.
+  - hauto l:on.
+  - hauto lq:on ctrs:nsteps inv:LoRed.R.
+Qed.
+
+Lemma lored_hne_preservation n (a b : PTm n) :
+    LoRed.R a b -> ishne a -> ishne b.
+Proof.  induction 1; sfirstorder. Qed.
+
+Lemma loreds_hne_preservation n (a b : PTm n) :
+  rtc LoRed.R a b -> ishne a -> ishne b.
+Proof. induction 1; hauto lq:on ctrs:rtc use:lored_hne_preservation. Qed.
+
+Lemma lored_nsteps_bind_inv k n p (a0 : PTm n) b0 C :
+    nsteps LoRed.R k (PBind p a0 b0) C ->
+    exists i j a1 b1,
+      i <= k /\ j <= k /\
+        C = PBind p a1 b1 /\
+        nsteps LoRed.R i a0 a1 /\
+        nsteps LoRed.R j b0 b1.
+Proof.
+  move E : (PBind p a0 b0) => u hu. move : p a0 b0 E.
+  elim : k u C / hu.
+  - sauto lq:on.
+  - move => k a0 a1 a2 ha ha' ih p a3 b0 ?. subst.
+    inversion ha; subst => //=;
+    spec_refl.
+    move : ih => [i][j][a1][b1][?][?][?][h0]h1. subst.
+    exists (S i),j,a1,b1. sauto lq:on solve+:lia.
+    move : ih => [i][j][a1][b1][?][?][?][h0]h1. subst.
+    exists i,(S j),a1,b1. sauto lq:on solve+:lia.
+Qed.
+
+Lemma lored_nsteps_app_inv k n (a0 b0 C : PTm n) :
+    nsteps LoRed.R k (PApp a0 b0) C ->
+    ishne a0 ->
+    exists i j a1 b1,
+      i <= k /\ j <= k /\
+        C = PApp a1 b1 /\
+        nsteps LoRed.R i a0 a1 /\
+        nsteps LoRed.R j b0 b1.
+Proof.
+  move E : (PApp a0 b0) => u hu. move : a0 b0 E.
+  elim : k u C / hu.
+  - sauto lq:on.
+  - move => k a0 a1 a2 ha01 ha12 ih a3 b0 ?.  subst.
+    inversion ha01; subst => //=.
+    spec_refl.
+    move => h.
+    have : ishne a4 by sfirstorder use:lored_hne_preservation.
+    move : ih => /[apply]. move => [i][j][a1][b1][?][?][?][h0]h1.
+    subst. exists (S i),j,a1,b1. sauto lq:on solve+:lia.
+    spec_refl. move : ih => /[apply].
+    move => [i][j][a1][b1][?][?][?][h0]h1. subst.
+    exists i, (S j), a1, b1. sauto lq:on solve+:lia.
+Qed.
+
+Lemma lored_nsteps_proj_inv k n p (a0 C : PTm n) :
+    nsteps LoRed.R k (PProj p a0) C ->
+    ishne a0 ->
+    exists i a1,
+      i <= k /\
+        C = PProj p a1 /\
+        nsteps LoRed.R i a0 a1.
+Proof.
+  move E : (PProj p a0) => u hu. move : a0 E.
+  elim : k u C / hu.
+  - sauto lq:on.
+  - move => k a0 a1 a2 ha01 ha12 ih a3 ?. subst.
+    inversion ha01; subst => //=.
+    spec_refl.
+    move => h.
+    have : ishne a4 by sfirstorder use:lored_hne_preservation.
+    move : ih => /[apply]. move => [i][a1][?][?]h0. subst.
+    exists (S i), a1. hauto lq:on ctrs:nsteps solve+:lia.
+Qed.
+
+Lemma algo_metric_proj n k p0 p1 (a0 a1 : PTm n) :
+  algo_metric k (PProj p0 a0) (PProj p1 a1) ->
+  ishne a0 ->
+  ishne a1 ->
+  p0 = p1 /\ exists j, j < k /\ algo_metric j a0 a1.
+Proof.
+  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 hne0 hne1.
+  move : lored_nsteps_proj_inv h0 (hne0);repeat move/[apply].
+  move => [i0][a2][hi][?]ha02. subst.
+  move : lored_nsteps_proj_inv h1 (hne1);repeat move/[apply].
+  move => [i1][a3][hj][?]ha13. subst.
+  simpl in *.
+  move /EJoin.hne_proj_inj : h4 => [h40 h41]. subst.
+  split => //.
+  exists (k - 1). split. simpl in *; lia.
+  rewrite/algo_metric.
+  do 4 eexists. repeat split; eauto. sfirstorder use:ne_nf.
+  sfirstorder use:ne_nf.
+  lia.
+Qed.
+
+Lemma lored_nsteps_app_cong k n (a0 a1 b : PTm n) :
+  nsteps LoRed.R k a0 a1 ->
+  ishne a0 ->
+  nsteps LoRed.R k (PApp a0 b) (PApp a1 b).
+  move => h. move : b.
+  elim : k a0 a1 / h.
+  - sauto.
+  - move => m a0 a1 a2 h0 h1 ih.
+    move => b hneu.
+    apply : nsteps_l; eauto using LoRed.AppCong0.
+    apply LoRed.AppCong0;eauto. move : hneu. clear. case : a0 => //=.
+    apply ih. sfirstorder use:lored_hne_preservation.
+Qed.
+
+Lemma lored_nsteps_proj_cong k n p (a0 a1 : PTm n) :
+  nsteps LoRed.R k a0 a1 ->
+  ishne a0 ->
+  nsteps LoRed.R k (PProj p a0) (PProj p a1).
+  move => h. move : p.
+  elim : k a0 a1 / h.
+  - sauto.
+  - move => m a0 a1 a2 h0 h1 ih p hneu.
+    apply : nsteps_l; eauto using LoRed.ProjCong.
+    apply LoRed.ProjCong;eauto. move : hneu. clear. case : a0 => //=.
+    apply ih. sfirstorder use:lored_hne_preservation.
+Qed.
+
+Lemma lored_nsteps_pair_inv k n (a0 b0 C : PTm n) :
+    nsteps LoRed.R k (PPair a0 b0) C ->
+    exists i j a1 b1,
+      i <= k /\ j <= k /\
+        C = PPair a1 b1 /\
+        nsteps LoRed.R i a0 a1 /\
+        nsteps LoRed.R j b0 b1.
+  move E : (PPair a0 b0) => u hu. move : a0 b0 E.
+  elim : k u C / hu.
+  - sauto lq:on.
+  - move => k a0 a1 a2 ha01 ha12 ih a3 b0 ?.  subst.
+    inversion ha01; subst => //=.
+    spec_refl.
+    move : ih => [i][j][a1][b1][?][?][?][h0]h1.
+    subst. exists (S i),j,a1,b1. sauto lq:on solve+:lia.
+    spec_refl.
+    move : ih => [i][j][a1][b1][?][?][?][h0]h1. subst.
+    exists i, (S j), a1, b1. sauto lq:on solve+:lia.
+Qed.
+
+Lemma algo_metric_join n k (a b : PTm n) :
+  algo_metric k a b ->
+  DJoin.R a b.
+  rewrite /algo_metric.
+  move => [i][j][va][vb][h0][h1][h2][h3][[v [h40 h41]]]h5.
+  have {}h0 : rtc LoRed.R a va by hauto lq:on use:@relations.rtc_nsteps.
+  have {}h1 : rtc LoRed.R b vb by hauto lq:on use:@relations.rtc_nsteps.
+  apply REReds.FromEReds in h40,h41.
+  apply LoReds.ToRReds in h0,h1.
+  apply REReds.FromRReds in h0,h1.
+  rewrite /DJoin.R. exists v. sfirstorder use:@relations.rtc_transitive.
+Qed.
+
+Lemma algo_metric_pair n k (a0 b0 a1 b1 : PTm n) :
+  SN (PPair a0 b0) ->
+  SN (PPair a1 b1) ->
+  algo_metric k (PPair a0 b0) (PPair a1 b1) ->
+  exists j, j < k /\ algo_metric j a0 a1 /\ algo_metric j b0 b1.
+  move => sn0 sn1 /[dup] /algo_metric_join hj.
+  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
+  move : lored_nsteps_pair_inv h0;repeat move/[apply].
+  move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
+  move : lored_nsteps_pair_inv h1;repeat move/[apply].
+  move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
+  simpl in *. exists (k - 1).
+  move /andP : h2 => [h20 h21].
+  move /andP : h3 => [h30 h31].
+  suff : EJoin.R a2 a3 /\ EJoin.R b2 b3 by hauto lq:on solve+:lia.
+  hauto l:on use:DJoin.ejoin_pair_inj.
+Qed.
+
+Lemma hne_nf_ne n (a : PTm n) :
+  ishne a -> nf a -> ne a.
+Proof. case : a => //=. Qed.
+
+Lemma lored_nsteps_renaming k n m (a b : PTm n) (ξ : fin n -> fin m) :
+  nsteps LoRed.R k a b ->
+  nsteps LoRed.R k (ren_PTm ξ a) (ren_PTm ξ b).
+Proof.
+  induction 1; hauto lq:on ctrs:nsteps use:LoRed.renaming.
+Qed.
+
+Lemma algo_metric_neu_abs n k (a0 : PTm (S n)) u :
+  algo_metric k u (PAbs a0) ->
+  ishne u ->
+  exists j, j < k /\ algo_metric j (PApp (ren_PTm shift u) (VarPTm var_zero)) a0.
+Proof.
+  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 neu.
+  have neva : ne va by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
+  move /lored_nsteps_abs_inv : h1 => [a1][h01]?. subst.
+  exists (k - 1). simpl in *. split. lia.
+  have {}h0 : nsteps LoRed.R i (ren_PTm shift u) (ren_PTm shift va)
+    by eauto using lored_nsteps_renaming.
+  have {}h0 : nsteps LoRed.R i (PApp (ren_PTm shift u) (VarPTm var_zero)) (PApp (ren_PTm shift va) (VarPTm var_zero)).
+  apply lored_nsteps_app_cong => //=.
+  scongruence use:ishne_ren.
+  do 4 eexists. repeat split; eauto.
+  hauto b:on use:ne_nf_ren.
+  have h : EJoin.R (PAbs (PApp (ren_PTm shift va) (VarPTm var_zero))) (PAbs a1) by hauto q:on ctrs:rtc,ERed.R.
+  apply DJoin.ejoin_abs_inj; eauto.
+  hauto b:on drew:off use:ne_nf_ren.
+  simpl in *.  rewrite size_PTm_ren. lia.
+Qed.
+
+Lemma algo_metric_neu_pair n k (a0 b0 : PTm n) u :
+  algo_metric k u (PPair a0 b0) ->
+  ishne u ->
+  exists j, j < k /\ algo_metric j (PProj PL u) a0 /\ algo_metric j (PProj PR u) b0.
+Proof.
+  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 neu.
+  move /lored_nsteps_pair_inv : h1.
+  move => [i0][j0][a1][b1][hi][hj][?][ha01]hb01. subst.
+  simpl in *.
+  have ? : ishne va by
+    hauto lq:on use:loreds_hne_preservation, @relations.rtc_nsteps.
+  have ? : ne va by sfirstorder use:hne_nf_ne.
+  exists (k - 1). split. lia.
+  move :lored_nsteps_proj_cong (neu) h0; repeat move/[apply].
+  move => h. have hL := h PL. have {h} hR := h PR.
+  suff [? ?] : EJoin.R (PProj PL va) a1  /\ EJoin.R (PProj PR va) b1.
+  rewrite /algo_metric.
+  split; do 4 eexists; repeat split;eauto; sfirstorder b:on solve+:lia.
+  eapply DJoin.ejoin_pair_inj; hauto qb:on ctrs:rtc, ERed.R.
+Qed.
+
+Lemma algo_metric_app n k (a0 b0 a1 b1 : PTm n) :
+  algo_metric k (PApp a0 b0) (PApp a1 b1) ->
+  ishne a0 ->
+  ishne a1 ->
+  exists j, j < k /\ algo_metric j a0 a1 /\ algo_metric j b0 b1.
+Proof.
+  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
+  move => hne0 hne1.
+  move : lored_nsteps_app_inv h0 (hne0);repeat move/[apply].
+  move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
+  move : lored_nsteps_app_inv h1 (hne1);repeat move/[apply].
+  move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
+  simpl in *. exists (k - 1).
+  move /andP : h2 => [h20 h21].
+  move /andP : h3 => [h30 h31].
+  move /EJoin.hne_app_inj : h4 => [h40 h41].
+  split. lia.
+  split.
+  + rewrite /algo_metric.
+    exists i0,j0,a2,a3.
+    repeat split => //=.
+    sfirstorder b:on use:ne_nf.
+    sfirstorder b:on use:ne_nf.
+    lia.
+  + rewrite /algo_metric.
+    exists i1,j1,b2,b3.
+    repeat split => //=; sfirstorder b:on use:ne_nf.
+Qed.
+
+Lemma algo_metric_bind n k p0 (A0 : PTm n) B0 p1 A1 B1  :
+  algo_metric k (PBind p0 A0 B0) (PBind p1 A1 B1) ->
+  p0 = p1 /\ exists j, j < k /\ algo_metric j A0 A1 /\ algo_metric j B0 B1.
+Proof.
+  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
+  move : lored_nsteps_bind_inv h0 => /[apply].
+  move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
+  move : lored_nsteps_bind_inv h1 => /[apply].
+  move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
+  move /EJoin.bind_inj : h4 => [?][hEa]hEb. subst.
+  split => //.
+  exists (k - 1). split. simpl in *; lia.
+  simpl in *.
+  split.
+  - exists i0,j0,a2,a3.
+    repeat split => //=; sfirstorder b:on solve+:lia.
+  - exists i1,j1,b2,b3. sfirstorder b:on solve+:lia.
+Qed.
+
+Lemma T_Univ_Raise n Γ (a : PTm n) i j :
+  Γ ⊢ a ∈ PUniv i ->
+  i <= j ->
+  Γ ⊢ a ∈ PUniv j.
+Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed.
+
+Lemma Abs_Pi_Inv n Γ (a : PTm (S n)) A B :
+  Γ ⊢ PAbs a ∈ PBind PPi A B ->
+  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B.
+Proof.
+  move => h.
+  have [i hi] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by hauto use:regularity.
+  have  [{}i {}hi] : exists i, Γ ⊢ A ∈ PUniv i by hauto use:Bind_Inv.
+  apply : subject_reduction; last apply RRed.AppAbs'.
+  apply : T_App'; cycle 1.
+  apply : weakening_wt'; cycle 2. apply hi.
+  apply h. reflexivity. reflexivity. rewrite -/ren_PTm.
+  apply T_Var' with (i := var_zero).  by asimpl.
+  by eauto using Wff_Cons'.
+  rewrite -/ren_PTm.
+  by asimpl.
+  rewrite -/ren_PTm.
+  by asimpl.
+Qed.
+
+Lemma Pair_Sig_Inv n Γ (a b : PTm n) A B :
+  Γ ⊢ PPair a b ∈ PBind PSig A B ->
+  Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B.
+Proof.
+  move => /[dup] h0 h1.
+  have [i hr] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by sfirstorder use:regularity.
+  move /T_Proj1 in h0.
+  move /T_Proj2 in h1.
+  split.
+  hauto lq:on use:subject_reduction ctrs:RRed.R.
+  have hE : Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A by
+    hauto lq:on use:RRed_Eq ctrs:RRed.R.
+  apply : T_Conv.
+  move /subject_reduction : h1. apply.
+  apply RRed.ProjPair.
+  apply : bind_inst; eauto.
+Qed.
+
+Lemma coqeq_complete' n k (a b : PTm n) :
+  algo_metric k a b ->
+  (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\
+  (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C).
+Proof.
+  move : k n a b.
+  elim /Wf_nat.lt_wf_ind.
+  move => n ih.
+  move => k a b /[dup] h /algo_metric_case. move : k a b h => [:hstepL].
+  move => k a b h.
+  (* Cases where a and b can take steps *)
+  case; cycle 1.
+  move : k a b h.
+  abstract : hstepL. qauto l:on use:HRed.preservation, CE_HRedL, hred_hne.
+  move  /algo_metric_sym /algo_metric_case : (h).
+  case; cycle 1.
+  move {ih}. move /algo_metric_sym : h.
+  move : hstepL => /[apply].
+  hauto lq:on use:coqeq_symmetric_mutual, algo_metric_sym.
+  (* Cases where a and b can't take wh steps *)
+  move {hstepL}.
+  move : k a b h. move => [:hnfneu].
+  move => k a b h.
+  case => fb; case => fa.
+  - split; last by sfirstorder use:hf_not_hne.
+    move {hnfneu}.
+    case : a h fb fa => //=.
+    + case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_AbsBind_Imp, T_AbsUniv_Imp.
+      move => a0 a1 ha0 _ _ Γ A wt0 wt1.
+      move : T_Abs_Inv wt0 wt1; repeat move/[apply]. move  => [Δ [V [wt1 wt0]]].
+      apply : CE_HRed; eauto using rtc_refl.
+      apply CE_AbsAbs.
+      suff [l [h0 h1]] : exists l, l < n /\ algo_metric l a1 a0 by eapply ih; eauto.
+      have ? : n > 0 by sauto solve+:lia.
+      exists (n - 1). split; first by lia.
+      move : (ha0). rewrite /algo_metric.
+      move => [i][j][va][vb][hr0][hr1][nfva][nfvb][[v [hr0' hr1']]] har.
+      apply lored_nsteps_abs_inv in hr0, hr1.
+      move : hr0 => [va' [hr00 hr01]].
+      move : hr1 => [vb' [hr10 hr11]]. move {ih}.
+      exists i,j,va',vb'. subst.
+      suff [v0 [hv00 hv01]] : exists v0, rtc ERed.R va' v0 /\ rtc ERed.R vb' v0.
+      repeat split =>//=. sfirstorder.
+      simpl in *; by lia.
+      move /algo_metric_join /DJoin.symmetric : ha0.
+      have : SN a0 /\ SN a1 by qauto l:on use:fundamental_theorem, logrel.SemWt_SN.
+      move => /[dup] [[ha00 ha10]] [].
+      move : DJoin.abs_inj; repeat move/[apply].
+      move : DJoin.standardization ha00 ha10; repeat move/[apply].
+      (* this is awful *)
+      move => [vb][va][h' [h'' [h''' [h'''' h'''''']]]].
+      have /LoReds.ToRReds {}hr00 : rtc LoRed.R a1 va'
+        by hauto lq:on use:@relations.rtc_nsteps.
+      have /LoReds.ToRReds {}hr10 : rtc LoRed.R a0 vb'
+        by hauto lq:on use:@relations.rtc_nsteps.
+      simpl in *.
+      have [*] : va' = va /\ vb' = vb by eauto using red_uniquenf. subst.
+      sfirstorder.
+    + case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_PairBind_Imp, T_PairUniv_Imp.
+      move => a1 b1 a0 b0 h _ _ Γ A hu0 hu1.
+      have [sn0 sn1] : SN (PPair a0 b0) /\ SN (PPair a1 b1)
+        by qauto l:on use:fundamental_theorem, logrel.SemWt_SN.
+      apply : CE_HRed; eauto using rtc_refl.
+      move /Pair_Inv : hu0 => [A0][B0][ha0][hb0]hSu0.
+      move /Pair_Inv : hu1 => [A1][B1][ha1][hb1]hSu1.
+      move /Sub_Bind_InvR :  (hSu0).
+      move => [i][A2][B2]hE.
+      have hSu12 : Γ ⊢ PBind PSig A1 B1 ≲ PBind PSig A2 B2
+        by eauto using Su_Transitive, Su_Eq.
+      have hSu02 : Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A2 B2
+        by eauto using Su_Transitive, Su_Eq.
+      have hA02 : Γ ⊢ A0 ≲ A2 by eauto using Su_Sig_Proj1.
+      have hA12 : Γ ⊢ A1 ≲ A2 by eauto using Su_Sig_Proj1.
+      have ha0A2 : Γ ⊢ a0 ∈ A2 by eauto using T_Conv.
+      have ha1A2 : Γ ⊢ a1 ∈ A2 by eauto using T_Conv.
+      move /algo_metric_pair : h sn0 sn1; repeat move/[apply].
+      move => [j][hj][ih0 ih1].
+      have haE : a0 ⇔ a1 by hauto l:on.
+      apply CE_PairPair => //.
+      have {}haE : Γ ⊢ a0 ≡ a1 ∈ A2
+        by hauto l:on use:coqeq_sound_mutual.
+      have {}hb1 : Γ ⊢ b1 ∈ subst_PTm (scons a1 VarPTm) B2.
+      apply : T_Conv; eauto.
+      move /E_Refl in ha1. hauto l:on use:Su_Sig_Proj2.
+      eapply ih; cycle -1; eauto.
+      apply : T_Conv; eauto.
+      apply Su_Transitive with (B := subst_PTm (scons a0 VarPTm) B2).
+      move /E_Refl in ha0. hauto l:on use:Su_Sig_Proj2.
+      move : hE haE. clear.
+      move => h.
+      eapply regularity in h.
+      move : h => [_ [hB _]].
+      eauto using bind_inst.
+    + case : b => //=.
+      * hauto lq:on use:T_AbsBind_Imp.
+      * hauto lq:on rew:off use:T_PairBind_Imp.
+      * move => p1 A1 B1 p0 A0 B0.
+        move /algo_metric_bind.
+        move => [?][j [ih0 [ih1 ih2]]]_ _. subst.
+        move => Γ A hU0 hU1.
+        move /Bind_Inv : hU0 => [i0 [hA0 [hB0 hS0]]].
+        move /Bind_Inv : hU1 => [i1 [hA1 [hB1 hS1]]].
+        have ? : Γ ⊢ PUniv i0 ≲ PUniv (max i0 i1)
+          by hauto lq:on rew:off use:Su_Univ, wff_mutual solve+:lia.
+        have ? : Γ ⊢ PUniv i1 ≲ PUniv (max i0 i1)
+          by hauto lq:on rew:off use:Su_Univ, wff_mutual solve+:lia.
+        have {}hA0 : Γ ⊢ A0 ∈ PUniv (max i0 i1) by eauto using T_Conv.
+        have {}hA1 : Γ ⊢ A1 ∈ PUniv (max i0 i1) by eauto using T_Conv.
+        have {}hB0 : funcomp (ren_PTm shift) (scons A0 Γ) ⊢
+                       B0 ∈ PUniv (max i0 i1)
+          by hauto lq:on use:T_Univ_Raise solve+:lia.
+        have {}hB1 : funcomp (ren_PTm shift) (scons A1 Γ) ⊢
+                       B1 ∈ PUniv (max i0 i1)
+          by hauto lq:on use:T_Univ_Raise solve+:lia.
+
+        have ihA : A0 ⇔ A1 by hauto l:on.
+        have hAE : Γ ⊢ A0 ≡ A1 ∈ PUniv (Nat.max i0 i1)
+          by hauto l:on use:coqeq_sound_mutual.
+        apply : CE_HRed; eauto using rtc_refl.
+        constructor => //.
+
+        eapply ih; eauto.
+        apply : ctx_eq_subst_one; eauto.
+        eauto using Su_Eq.
+      * move => > /algo_metric_join.
+        hauto lq:on use:DJoin.bind_univ_noconf.
+    + case : b => //=.
+      * hauto lq:on use:T_AbsUniv_Imp.
+      * hauto lq:on use:T_PairUniv_Imp.
+      * qauto l:on use:algo_metric_join, DJoin.bind_univ_noconf, DJoin.symmetric.
+      * move => i j /algo_metric_join /DJoin.univ_inj ? _ _ Γ A hi hj.
+        subst.
+        hauto l:on.
+  - move : k a b h fb fa. abstract : hnfneu.
+    move => k.
+    move => + b.
+    case : b => //=.
+    (* NeuAbs *)
+    + move => a u halg _ nea. split => // Γ A hu /[dup] ha.
+      move /Abs_Inv => [A0][B0][_]hSu.
+      move /Sub_Bind_InvR : (hSu) => [i][A2][B2]hE.
+      have {}hu : Γ ⊢ u ∈ PBind PPi A2 B2 by eauto using T_Conv_E.
+      have {}ha : Γ ⊢ PAbs a ∈ PBind PPi A2 B2 by eauto using T_Conv_E.
+      have {}hE : Γ ⊢ PBind PPi A2 B2 ∈ PUniv i
+        by hauto l:on use:regularity.
+      have {i} [j {}hE] : exists j, Γ ⊢ A2 ∈ PUniv j
+          by qauto l:on use:Bind_Inv.
+      have hΓ : ⊢ funcomp (ren_PTm shift) (scons A2 Γ) by eauto using Wff_Cons'.
+      set Δ := funcomp _ _ in hΓ.
+      have {}hu : Δ ⊢ PApp (ren_PTm shift u) (VarPTm var_zero) ∈ B2.
+      apply : T_App'; cycle 1. apply : weakening_wt' => //=; eauto.
+      reflexivity.
+      rewrite -/ren_PTm.
+      by apply T_Var.
+      rewrite -/ren_PTm. by asimpl.
+      move /Abs_Pi_Inv in ha.
+      move /algo_metric_neu_abs /(_ nea) : halg.
+      move => [j0][hj0]halg.
+      apply : CE_HRed; eauto using rtc_refl.
+      eapply CE_NeuAbs => //=.
+      eapply ih; eauto.
+    (* NeuPair *)
+    + move => a0 b0 u halg _ neu.
+      split => // Γ A hu /[dup] wt.
+      move /Pair_Inv => [A0][B0][ha0][hb0]hU.
+      move /Sub_Bind_InvR : (hU) => [i][A2][B2]hE.
+      have {}wt : Γ ⊢ PPair a0 b0 ∈ PBind PSig A2 B2 by sauto lq:on.
+      have {}hu : Γ ⊢ u ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
+      move /Pair_Sig_Inv : wt => [{}ha0 {}hb0].
+      have /T_Proj1 huL := hu.
+      have /T_Proj2 {hu} huR := hu.
+      move /algo_metric_neu_pair /(_ neu) : halg => [j [hj [hL hR]]].
+      have heL : PProj PL u ⇔ a0 by hauto l:on.
+      eapply CE_HRed; eauto using rtc_refl.
+      apply CE_NeuPair; eauto.
+      eapply ih; eauto.
+      apply : T_Conv; eauto.
+      have {}hE : Γ ⊢ PBind PSig A2 B2 ∈ PUniv i
+        by hauto l:on use:regularity.
+      have /E_Symmetric : Γ ⊢ PProj PL u  ≡ a0 ∈ A2 by
+        hauto l:on use:coqeq_sound_mutual.
+      hauto l:on use:bind_inst.
+    (* NeuBind: Impossible *)
+    + move => b p p0 a /algo_metric_join h _ h0. exfalso.
+      move : h h0. clear.
+      move /Sub.FromJoin.
+      hauto l:on use:Sub.hne_bind_noconf.
+    (* NeuUniv: Impossible *)
+    + hauto lq:on rew:off use:DJoin.hne_univ_noconf, algo_metric_join.
+  - move {ih}.
+    move /algo_metric_sym in h.
+    qauto l:on use:coqeq_symmetric_mutual.
+  - move {hnfneu}.
+
+    (* Clear out some trivial cases *)
+    suff : (forall (Γ : fin k -> PTm k) (A B : PTm k), Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ (exists C : PTm k, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C)).
+    move => h0.
+    split. move => *. apply : CE_HRed; eauto using rtc_refl. apply CE_NeuNeu. by firstorder.
+    by firstorder.
+
+    case : a h fb fa => //=.
+    + case : b => //=.
+      move => i j hi _ _.
+      * have ? : j = i by hauto lq:on use:algo_metric_join, DJoin.var_inj. subst.
+        move => Γ A B hA hB.
+        split. apply CE_VarCong.
+        exists (Γ i). hauto l:on use:Var_Inv, T_Var.
+      * move => p p0 f /algo_metric_join. clear => ? ? _. exfalso.
+        hauto l:on use:REReds.var_inv, REReds.hne_app_inv.
+      * move => a0 a1 i /algo_metric_join. clear => ? ? _. exfalso.
+        hauto l:on use:REReds.var_inv, REReds.hne_proj_inv.
+      * sfirstorder use:T_Bot_Imp.
+    + case : b => //=.
+      * clear. move => i a a0 /algo_metric_join h _ ?. exfalso.
+        hauto l:on use:REReds.hne_app_inv, REReds.var_inv.
+      (* real case *)
+      * move => b1 a1 b0 a0 halg hne1 hne0 Γ A B wtA wtB.
+        move /App_Inv : wtA => [A0][B0][hb0][ha0]hS0.
+        move /App_Inv : wtB => [A1][B1][hb1][ha1]hS1.
+        move : algo_metric_app (hne0) (hne1) halg. repeat move/[apply].
+        move => [j [hj [hal0 hal1]]].
+        have /ih := hal0.
+        move /(_ hj).
+        move => [_ ihb].
+        move : ihb (hne0) (hne1) hb0 hb1. repeat move/[apply].
+        move => [hb01][C][hT0][hT1][hT2]hT3.
+        move /Sub_Bind_InvL : (hT0).
+        move => [i][A2][B2]hE.
+        have hSu20 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A0 B0 by
+          eauto using Su_Eq, Su_Transitive.
+        have hSu10 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A1 B1 by
+          eauto using Su_Eq, Su_Transitive.
+        have hSuA0 : Γ ⊢ A0 ≲ A2 by sfirstorder use:Su_Pi_Proj1.
+        have hSuA1 : Γ ⊢ A1 ≲ A2 by sfirstorder use:Su_Pi_Proj1.
+        have ha1' : Γ ⊢ a1 ∈ A2 by eauto using T_Conv.
+        have ha0' : Γ ⊢ a0 ∈ A2 by eauto using T_Conv.
+        move : ih (hj) hal1. repeat move/[apply].
+        move => [ih _].
+        move : ih (ha0') (ha1'); repeat move/[apply].
+        move => iha.
+        split. sauto lq:on.
+        exists (subst_PTm (scons a0 VarPTm) B2).
+        split.
+        apply : Su_Transitive; eauto.
+        move /E_Refl in ha0.
+        hauto l:on use:Su_Pi_Proj2.
+        have h01 : Γ ⊢ a0 ≡ a1 ∈ A2 by sfirstorder use:coqeq_sound_mutual.
+        split.
+        apply Su_Transitive with (B := subst_PTm (scons a1 VarPTm) B2).
+        move /regularity_sub0 : hSu10 => [i0].
+        hauto l:on use:bind_inst.
+        hauto lq:on rew:off use:Su_Pi_Proj2, Su_Transitive, E_Refl.
+        split.
+        by apply : T_App; eauto using T_Conv_E.
+        apply : T_Conv; eauto.
+        apply T_App with (A := A2) (B := B2); eauto.
+        apply : T_Conv_E; eauto.
+        move /E_Symmetric in h01.
+        move /regularity_sub0 : hSu20 => [i0].
+        sfirstorder use:bind_inst.
+      * move => p p0 p1 p2 /algo_metric_join. clear => ? ? ?. exfalso.
+        hauto q:on use:REReds.hne_app_inv, REReds.hne_proj_inv.
+      * sfirstorder use:T_Bot_Imp.
+    + case : b => //=.
+      * move => i p h /algo_metric_join. clear => ? _ ?. exfalso.
+        hauto l:on use:REReds.hne_proj_inv, REReds.var_inv.
+      * move => > /algo_metric_join. clear => ? ? ?. exfalso.
+        hauto l:on use:REReds.hne_proj_inv, REReds.hne_app_inv.
+      (* real case *)
+      * move => p1 a1 p0 a0 /algo_metric_proj ha hne1 hne0.
+        move : ha (hne0) (hne1); repeat move/[apply].
+        move => [? [j []]]. subst.
+        move : ih; repeat move/[apply].
+        move => [_ ih].
+        case : p1.
+        ** move => Γ A B ha0 ha1.
+           move /Proj1_Inv : ha0. move => [A0][B0][ha0]hSu0.
+           move /Proj1_Inv : ha1. move => [A1][B1][ha1]hSu1.
+           move : ih ha0 ha1 (hne0) (hne1); repeat move/[apply].
+           move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
+           split. sauto lq:on.
+           move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2.
+           have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0
+             by eauto using Su_Transitive, Su_Eq.
+           have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1
+             by eauto using Su_Transitive, Su_Eq.
+           exists A2. split; eauto using Su_Sig_Proj1, Su_Transitive.
+           repeat split => //=.
+           hauto l:on use:Su_Sig_Proj1, Su_Transitive.
+           apply T_Proj1 with (B := B2); eauto using T_Conv_E.
+           apply T_Proj1 with (B := B2); eauto using T_Conv_E.
+        ** move => Γ A B  ha0  ha1.
+           move /Proj2_Inv : ha0. move => [A0][B0][ha0]hSu0.
+           move /Proj2_Inv : ha1. move => [A1][B1][ha1]hSu1.
+           move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply].
+           move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
+           split. sauto lq:on.
+           move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2.
+           have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0
+             by eauto using Su_Transitive, Su_Eq.
+           have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1
+             by eauto using Su_Transitive, Su_Eq.
+           have hA20 : Γ ⊢ A2 ≲ A0 by eauto using Su_Sig_Proj1.
+           have hA21 : Γ ⊢ A2 ≲ A1 by eauto using Su_Sig_Proj1.
+           have {}wta0 : Γ ⊢ a0 ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
+           have {}wta1 : Γ ⊢ a1 ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
+           have haE : Γ ⊢ PProj PL a0 ≡ PProj PL a1 ∈ A2
+             by sauto lq:on use:coqeq_sound_mutual.
+           exists (subst_PTm (scons (PProj PL a0) VarPTm) B2).
+           repeat split.
+           *** apply : Su_Transitive; eauto.
+               have : Γ ⊢ PProj PL a0 ≡ PProj PL a0 ∈ A2
+                 by qauto use:regularity, E_Refl.
+               sfirstorder use:Su_Sig_Proj2.
+           *** apply : Su_Transitive; eauto.
+               sfirstorder use:Su_Sig_Proj2.
+           *** eauto using T_Proj2.
+           *** apply : T_Conv.
+               apply : T_Proj2; eauto.
+               move /E_Symmetric in haE.
+               move /regularity_sub0 in hSu21.
+               sfirstorder use:bind_inst.
+      * sfirstorder use:T_Bot_Imp.
+    + sfirstorder use:T_Bot_Imp.
+Qed.
+
+Lemma coqeq_sound : forall n Γ (a b : PTm n) A,
+    Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b -> Γ ⊢ a ≡ b ∈ A.
+Proof. sfirstorder use:coqeq_sound_mutual. Qed.
+
+Lemma coqeq_complete n Γ (a b A : PTm n) :
+  Γ ⊢ a ≡ b ∈ A -> a ⇔ b.
+Proof.
+  move => h.
+  suff : exists k, algo_metric k a b by hauto lq:on use:coqeq_complete', regularity.
+  eapply fundamental_theorem in h.
+  move /logrel.SemEq_SN_Join : h.
+  move => h.
+  have : exists va vb : PTm n,
+         rtc LoRed.R a va /\
+         rtc LoRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb
+      by hauto l:on use:DJoin.standardization_lo.
+  move => [va][vb][hva][hvb][nva][nvb]hj.
+  move /relations.rtc_nsteps : hva => [i hva].
+  move /relations.rtc_nsteps : hvb => [j hvb].
+  exists (i + j + size_PTm va + size_PTm vb).
+  hauto lq:on solve+:lia.
+Qed.
diff --git a/theories/common.v b/theories/common.v
index 6ad3d44..24e708e 100644
--- a/theories/common.v
+++ b/theories/common.v
@@ -60,6 +60,7 @@ Fixpoint ishne {n} (a : PTm n) :=
   | VarPTm _ => true
   | PApp a _ => ishne a
   | PProj _ a => ishne a
+  | PBot => true
   | _ => false
   end.
 
@@ -90,3 +91,7 @@ Proof. case : a => //=. Qed.
 Definition ispair_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
   ispair (ren_PTm ξ a) = ispair a.
 Proof. case : a => //=. Qed.
+
+Definition ishne_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+  ishne (ren_PTm ξ a) = ishne a.
+Proof. move : m ξ. elim : n / a => //=. Qed.
diff --git a/theories/fp_red.v b/theories/fp_red.v
index beed0bb..b8bcc41 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -20,7 +20,7 @@ Ltac2 spec_refl () :=
                try (specialize $h with (1 := eq_refl))
            end)  (Control.hyps ()).
 
-Ltac spec_refl := ltac2:(spec_refl ()).
+Ltac spec_refl := ltac2:(Control.enter spec_refl).
 
 Module EPar.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
@@ -262,6 +262,12 @@ end.
 Lemma ne_nf n a : @ne n a -> nf a.
 Proof. elim : a => //=. Qed.
 
+Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) :
+  (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)).
+Proof.
+  move : m ξ. elim : n / a => //=; solve [hauto b:on].
+Qed.
+
 Inductive TRedSN' {n} (a : PTm n) : PTm n -> Prop :=
 | T_Refl :
   TRedSN' a a
@@ -293,6 +299,12 @@ Proof.
   apply N_β'. by asimpl. eauto.
 Qed.
 
+Lemma ne_nf_embed n (a : PTm n) :
+  (ne a -> SNe a) /\ (nf a -> SN a).
+Proof.
+  elim : n  / a => //=; hauto qb:on ctrs:SNe, SN.
+Qed.
+
 #[export]Hint Constructors SN SNe TRedSN : sn.
 
 Ltac2 rec solve_anti_ren () :=
@@ -836,12 +848,6 @@ Module RReds.
 End RReds.
 
 
-Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) :
-  (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)).
-Proof.
-  move : m ξ. elim : n / a => //=; solve [hauto b:on].
-Qed.
-
 Module NeEPar.
   Inductive R_nonelim {n} : PTm n -> PTm n ->  Prop :=
   (****************** Eta ***********************)
@@ -1440,6 +1446,14 @@ Module ERed.
     all : hauto lq:on ctrs:R.
   Qed.
 
+  Lemma nf_preservation n (a b : PTm n) :
+    ERed.R a b -> (nf a -> nf b) /\ (ne a -> ne b).
+  Proof.
+    move => h.
+    elim : n a b /h => //=;
+                        hauto lqb:on use:ne_nf_ren,ne_nf.
+  Qed.
+
 End ERed.
 
 Module EReds.
@@ -1510,10 +1524,70 @@ Module EReds.
     induction 1; hauto lq:on ctrs:rtc use:ERed.substing.
   Qed.
 
+  Lemma app_inv n (a0 b0 C : PTm n) :
+    rtc ERed.R (PApp a0 b0) C ->
+    exists a1 b1, C = PApp a1 b1 /\
+               rtc ERed.R a0 a1 /\
+               rtc ERed.R b0 b1.
+  Proof.
+    move E : (PApp a0 b0) => u hu.
+    move : a0 b0 E.
+    elim : u C / hu.
+    - hauto lq:on ctrs:rtc.
+    - move => a b c ha ha' iha a0 b0 ?. subst.
+      hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R.
+  Qed.
+
+  Lemma proj_inv n p (a C : PTm n) :
+    rtc ERed.R (PProj p a) C ->
+    exists c, C = PProj p c /\ rtc ERed.R a c.
+  Proof.
+    move E : (PProj p a) => u hu.
+    move : p a E.
+    elim : u C /hu;
+      hauto q:on ctrs:rtc,ERed.R inv:ERed.R.
+  Qed.
+
+  Lemma bind_inv n p (A : PTm n) B C :
+    rtc ERed.R (PBind p A B) C ->
+    exists A0 B0, C = PBind p A0 B0 /\ rtc ERed.R A A0 /\ rtc ERed.R B B0.
+  Proof.
+    move E : (PBind p A B) => u hu.
+    move : p A B E.
+    elim : u C / hu.
+    hauto lq:on ctrs:rtc.
+    hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R, rtc.
+  Qed.
+
 End EReds.
 
 #[export]Hint Constructors ERed.R RRed.R EPar.R : red.
 
+Module EJoin.
+  Definition R {n} (a b : PTm n) := exists c, rtc ERed.R a c /\ rtc ERed.R b c.
+
+  Lemma hne_app_inj n (a0 b0 a1 b1 : PTm n) :
+    R (PApp a0 b0) (PApp a1 b1) ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    hauto lq:on use:EReds.app_inv.
+  Qed.
+
+  Lemma hne_proj_inj n p0 p1 (a0 a1 : PTm n) :
+    R (PProj p0 a0) (PProj p1 a1) ->
+    p0 = p1 /\ R a0 a1.
+  Proof.
+    hauto lq:on rew:off use:EReds.proj_inv.
+  Qed.
+
+  Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
+    R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
+    p0 = p1 /\ R A0 A1 /\ R B0 B1.
+  Proof.
+    hauto lq:on rew:off use:EReds.bind_inv.
+  Qed.
+
+End EJoin.
 
 Module RERed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
@@ -1602,9 +1676,17 @@ Module RERed.
     hauto q:on use:ToBetaEta, FromBeta, FromEta, RRed.substing, ERed.substing.
   Qed.
 
+  Lemma hne_preservation n (a b : PTm n) :
+    RERed.R a b -> ishne a -> ishne b.
+  Proof.  induction 1; sfirstorder. Qed.
+
 End RERed.
 
 Module REReds.
+  Lemma hne_preservation n (a b : PTm n) :
+    rtc RERed.R a b -> ishne a -> ishne b.
+  Proof.  induction 1; eauto using RERed.hne_preservation, rtc_refl, rtc. Qed.
+
   Lemma sn_preservation n (a b : PTm n) :
     rtc RERed.R a b ->
     SN a ->
@@ -1686,6 +1768,40 @@ Module REReds.
     hauto lq:on rew:off ctrs:rtc inv:RERed.R.
   Qed.
 
+  Lemma var_inv n (i : fin n) C :
+    rtc RERed.R (VarPTm i) C ->
+    C = VarPTm i.
+  Proof.
+    move E : (VarPTm i) => u hu.
+    move : i E. elim : u C /hu; hauto lq:on rew:off inv:RERed.R.
+  Qed.
+
+  Lemma hne_app_inv n (a0 b0 C : PTm n) :
+    rtc RERed.R (PApp a0 b0) C ->
+    ishne a0 ->
+    exists a1 b1, C = PApp a1 b1 /\
+               rtc RERed.R a0 a1 /\
+               rtc RERed.R b0 b1.
+  Proof.
+    move E : (PApp a0 b0) => u hu.
+    move : a0 b0 E.
+    elim : u C / hu.
+    - hauto lq:on ctrs:rtc.
+    - move => a b c ha ha' iha a0 b0 ?. subst.
+      hauto lq:on rew:off ctrs:rtc, RERed.R use:RERed.hne_preservation inv:RERed.R.
+  Qed.
+
+  Lemma hne_proj_inv n p (a C : PTm n) :
+    rtc RERed.R (PProj p a) C ->
+    ishne a ->
+    exists c, C = PProj p c /\ rtc RERed.R a c.
+  Proof.
+    move E : (PProj p a) => u hu.
+    move : p a E.
+    elim : u C /hu;
+      hauto q:on ctrs:rtc,RERed.R use:RERed.hne_preservation inv:RERed.R.
+  Qed.
+
   Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
     rtc RERed.R a b -> rtc RERed.R (subst_PTm ρ a) (subst_PTm ρ b).
   Proof.
@@ -1721,6 +1837,14 @@ Module REReds.
     hauto l:on use:substing.
   Qed.
 
+  Lemma ToEReds n (a b : PTm n) :
+    nf a ->
+    rtc RERed.R a b -> rtc ERed.R a b.
+  Proof.
+    move => + h.
+    induction h; hauto lq:on rew:off ctrs:rtc use:RERed.ToBetaEta, RReds.nf_refl, @rtc_once, ERed.nf_preservation.
+  Qed.
+
 End REReds.
 
 Module LoRed.
@@ -1776,6 +1900,22 @@ Module LoRed.
     RRed.R a b.
   Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.
 
+  Lemma AppAbs' n a (b : PTm n) u :
+    u = (subst_PTm (scons b VarPTm) a) ->
+    R (PApp (PAbs a) b)  u.
+  Proof. move => ->. apply AppAbs. Qed.
+
+  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+    R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
+  Proof.
+    move => h. move : m ξ.
+    elim : n a b /h.
+
+    move => n a b m ξ /=.
+    apply AppAbs'. by asimpl.
+    all : try qauto ctrs:R use:ne_nf_ren, ishf_ren.
+  Qed.
+
 End LoRed.
 
 Module LoReds.
@@ -2107,6 +2247,12 @@ Module DJoin.
   Lemma refl n (a : PTm n) : R a a.
   Proof. sfirstorder use:@rtc_refl unfold:R. Qed.
 
+  Lemma FromEJoin n (a b : PTm n) : EJoin.R a b -> DJoin.R a b.
+  Proof. hauto q:on use:REReds.FromEReds. Qed.
+
+  Lemma ToEJoin n (a b : PTm n) : nf a -> nf b -> DJoin.R a b -> EJoin.R a b.
+  Proof. hauto q:on use:REReds.ToEReds. Qed.
+
   Lemma symmetric n (a b : PTm n) : R a b -> R b a.
   Proof. sfirstorder unfold:R. Qed.
 
@@ -2180,6 +2326,17 @@ Module DJoin.
     case : c => //=; itauto.
   Qed.
 
+  Lemma hne_univ_noconf n (a b : PTm n) :
+    R a b -> ishne a -> isuniv b -> False.
+  Proof.
+    move => [c [h0 h1]] h2 h3.
+    have {h0 h1 h2 h3} : ishne c /\ isuniv c by
+      hauto l:on use:REReds.hne_preservation,
+          REReds.univ_preservation.
+    move => [].
+    case : c => //=.
+  Qed.
+
   Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
     DJoin.R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
     p0 = p1 /\ DJoin.R A0 A1 /\ DJoin.R B0 B1.
@@ -2188,12 +2345,34 @@ Module DJoin.
     hauto lq:on rew:off use:REReds.bind_inv.
   Qed.
 
+  Lemma var_inj n (i j : fin n) :
+    R (VarPTm i) (VarPTm j) -> i = j.
+  Proof. sauto lq:on rew:off use:REReds.var_inv unfold:R. Qed.
+
   Lemma univ_inj n i j :
     @R n (PUniv i) (PUniv j)  -> i = j.
   Proof.
     sauto lq:on rew:off use:REReds.univ_inv.
   Qed.
 
+  Lemma hne_app_inj n (a0 b0 a1 b1 : PTm n) :
+    R (PApp a0 b0) (PApp a1 b1) ->
+    ishne a0 ->
+    ishne a1 ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    hauto lq:on use:REReds.hne_app_inv.
+  Qed.
+
+  Lemma hne_proj_inj n p0 p1 (a0 a1 : PTm n) :
+    R (PProj p0 a0) (PProj p1 a1) ->
+    ishne a0 ->
+    ishne a1 ->
+    p0 = p1 /\ R a0 a1.
+  Proof.
+    sauto lq:on use:REReds.hne_proj_inv.
+  Qed.
+
   Lemma FromRRed0 n (a b : PTm n) :
     RRed.R a b -> R a b.
   Proof.
@@ -2224,6 +2403,14 @@ Module DJoin.
     hauto lq:on rew:off ctrs:rtc unfold:R use:REReds.substing.
   Qed.
 
+  Lemma renaming n m (a b : PTm n) (ρ : fin n -> fin m) :
+    R a b -> R (ren_PTm ρ a) (ren_PTm ρ b).
+  Proof. substify. apply substing. Qed.
+
+  Lemma weakening n (a b : PTm n)  :
+    R a b -> R (ren_PTm shift a) (ren_PTm shift b).
+  Proof. apply renaming. Qed.
+
   Lemma cong n m (a : PTm (S n)) c d (ρ : fin n -> PTm m) :
     R c d -> R (subst_PTm (scons c ρ) a) (subst_PTm (scons d ρ) a).
   Proof.
@@ -2232,6 +2419,116 @@ Module DJoin.
     hauto q:on ctrs:rtc inv:option use:REReds.cong.
   Qed.
 
+  Lemma pair_inj n (a0 a1 b0 b1 : PTm n) :
+    SN (PPair a0 b0) ->
+    SN (PPair a1 b1) ->
+    R (PPair a0 b0) (PPair a1 b1) ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    move => sn0 sn1.
+    have [? [? [? ?]]] : SN a0 /\ SN b0 /\ SN a1 /\ SN b1 by sfirstorder use:SN_NoForbid.P_PairInv.
+    have ? : SN (PProj PL (PPair a0 b0)) by hauto lq:on db:sn.
+    have ? : SN (PProj PR (PPair a0 b0)) by hauto lq:on db:sn.
+    have ? : SN (PProj PL (PPair a1 b1)) by hauto lq:on db:sn.
+    have ? : SN (PProj PR (PPair a1 b1)) by hauto lq:on db:sn.
+    have h0L : RRed.R (PProj PL (PPair a0 b0)) a0 by eauto with red.
+    have h0R : RRed.R (PProj PR (PPair a0 b0)) b0 by eauto with red.
+    have h1L : RRed.R (PProj PL (PPair a1 b1)) a1 by eauto with red.
+    have h1R : RRed.R (PProj PR (PPair a1 b1)) b1 by eauto with red.
+    move => h2.
+    move /ProjCong in h2.
+    have h2L := h2 PL.
+    have {h2}h2R := h2 PR.
+    move /FromRRed1 in h0L.
+    move /FromRRed0 in h1L.
+    move /FromRRed1 in h0R.
+    move /FromRRed0 in h1R.
+    split; eauto using transitive.
+  Qed.
+
+  Lemma ejoin_pair_inj n (a0 a1 b0 b1 : PTm n) :
+    nf a0 -> nf b0 -> nf a1 -> nf b1 ->
+    EJoin.R (PPair a0 b0) (PPair a1 b1) ->
+    EJoin.R a0 a1 /\ EJoin.R b0 b1.
+  Proof.
+    move => h0 h1 h2 h3 /FromEJoin.
+    have [? ?] : SN (PPair a0 b0) /\ SN (PPair a1 b1) by sauto lqb:on rew:off use:ne_nf_embed.
+    move => ?.
+    have : R a0 a1 /\ R b0 b1 by hauto l:on use:pair_inj.
+    hauto l:on use:ToEJoin.
+  Qed.
+
+  Lemma abs_inj n (a0 a1 : PTm (S n)) :
+    SN a0 -> SN a1 ->
+    R (PAbs a0) (PAbs a1) ->
+    R a0 a1.
+  Proof.
+    move => sn0 sn1.
+    move /weakening => /=.
+    move /AppCong. move /(_ (VarPTm var_zero) (VarPTm var_zero)).
+    move => /(_ ltac:(sfirstorder use:refl)).
+    move => h.
+    have /FromRRed1 h0 : RRed.R (PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a0)) (VarPTm var_zero)) a0 by apply RRed.AppAbs'; asimpl.
+    have /FromRRed0 h1 : RRed.R (PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a1)) (VarPTm var_zero)) a1 by apply RRed.AppAbs'; asimpl.
+    have sn0' := sn0.
+    have sn1' := sn1.
+    eapply sn_renaming with (ξ := (upRen_PTm_PTm shift)) in sn0.
+    eapply sn_renaming with (ξ := (upRen_PTm_PTm shift)) in sn1.
+    apply : transitive; try apply h0.
+    apply : N_Exp. apply N_β. sauto.
+    by asimpl.
+    apply : transitive; try apply h1.
+    apply : N_Exp. apply N_β. sauto.
+    by asimpl.
+    eauto.
+  Qed.
+
+  Lemma ejoin_abs_inj n (a0 a1 : PTm (S n)) :
+    nf a0 -> nf a1 ->
+    EJoin.R (PAbs a0) (PAbs a1) ->
+    EJoin.R a0 a1.
+  Proof.
+    move => h0 h1.
+    have [? [? [? ?]]] : SN a0 /\ SN a1 /\ SN (PAbs a0) /\ SN (PAbs a1) by sauto lqb:on rew:off use:ne_nf_embed.
+    move /FromEJoin.
+    move /abs_inj.
+    hauto l:on use:ToEJoin.
+  Qed.
+
+  Lemma standardization n (a b : PTm n) :
+    SN a -> SN b -> R a b ->
+    exists va vb, rtc RRed.R a va /\ rtc RRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb.
+  Proof.
+    move => h0 h1 [ab [hv0 hv1]].
+    have hv : SN ab by sfirstorder use:REReds.sn_preservation.
+    have : exists v, rtc RRed.R ab v  /\ nf v by hauto q:on use:LoReds.FromSN, LoReds.ToRReds.
+    move => [v [hv2 hv3]].
+    have : rtc RERed.R a v by hauto q:on use:@relations.rtc_transitive, REReds.FromRReds.
+    have : rtc RERed.R b v by hauto q:on use:@relations.rtc_transitive, REReds.FromRReds.
+    move : h0 h1 hv3. clear.
+    move => h0 h1 hv hbv hav.
+    move : rered_standardization (h0) hav. repeat move/[apply].
+    move => [a1 [ha0 ha1]].
+    move : rered_standardization (h1) hbv. repeat move/[apply].
+    move => [b1 [hb0 hb1]].
+    have [*] : nf a1 /\ nf b1 by sfirstorder use:NeEPars.R_nonelim_nf.
+    hauto q:on use:NeEPars.ToEReds unfold:EJoin.R.
+  Qed.
+
+  Lemma standardization_lo n (a b : PTm n) :
+    SN a -> SN b -> R a b ->
+    exists va vb, rtc LoRed.R a va /\ rtc LoRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb.
+  Proof.
+    move => /[dup] sna + /[dup] snb.
+    move : standardization; repeat move/[apply].
+    move => [va][vb][hva][hvb][nfva][nfvb]hj.
+    move /LoReds.FromSN : sna => [va' [hva' hva'0]].
+    move /LoReds.FromSN : snb => [vb' [hvb' hvb'0]].
+    exists va', vb'.
+    repeat split => //=.
+    have : va = va' /\ vb = vb' by sfirstorder use:red_uniquenf, LoReds.ToRReds.
+    case; congruence.
+  Qed.
 End DJoin.
 
 
@@ -2385,6 +2682,17 @@ Module Sub.
     qauto l:on inv:SNe.
   Qed.
 
+  Lemma hne_bind_noconf n (a b : PTm n) :
+    R a b -> ishne a -> isbind b -> False.
+  Proof.
+    rewrite /R.
+    move => [c[d] [? []]] h0 h1 h2 h3.
+    have : ishne c by eauto using REReds.hne_preservation.
+    have : isbind d by eauto using REReds.bind_preservation.
+    move : h1. clear. inversion 1; subst => //=.
+    clear. case : d => //=.
+  Qed.
+
   Lemma bind_sne_noconf n (a b : PTm n) :
     R a b -> SNe b -> isbind a -> False.
   Proof.
diff --git a/theories/soundness.v b/theories/soundness.v
index 8dd87da..b11dded 100644
--- a/theories/soundness.v
+++ b/theories/soundness.v
@@ -10,3 +10,6 @@ Theorem fundamental_theorem :
   apply wt_mutual; eauto with sem; [hauto l:on use:SE_Pair].
   Unshelve. all : exact 0.
 Qed.
+
+Lemma synsub_to_usub : forall n Γ (a b : PTm n), Γ ⊢ a ≲ b -> SN a /\ SN b /\ Sub.R a b.
+Proof. hauto lq:on rew:off use:fundamental_theorem, SemLEq_SN_Sub. Qed.