diff --git a/theories/algorithmic.v b/theories/algorithmic.v
index 444f49f..3046ced 100644
--- a/theories/algorithmic.v
+++ b/theories/algorithmic.v
@@ -1,11 +1,10 @@
 Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax
-  common typing preservation admissible fp_red structural soundness.
+  common typing preservation admissible fp_red structural.
 From Hammer Require Import Tactics.
 Require Import ssreflect ssrbool.
 Require Import Psatz.
-From stdpp Require Import relations (rtc(..), nsteps(..)).
+From stdpp Require Import relations (rtc(..)).
 Require Import Coq.Logic.FunctionalExtensionality.
-Require Import Cdcl.Itauto.
 
 Module HRed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
@@ -59,169 +58,6 @@ 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).
@@ -309,14 +145,6 @@ 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
@@ -330,6 +158,23 @@ 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 *)
 
@@ -539,810 +384,3 @@ 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 24e708e..6ad3d44 100644
--- a/theories/common.v
+++ b/theories/common.v
@@ -60,7 +60,6 @@ Fixpoint ishne {n} (a : PTm n) :=
   | VarPTm _ => true
   | PApp a _ => ishne a
   | PProj _ a => ishne a
-  | PBot => true
   | _ => false
   end.
 
@@ -91,7 +90,3 @@ 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 b8bcc41..beed0bb 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:(Control.enter spec_refl).
+Ltac spec_refl := ltac2:(spec_refl ()).
 
 Module EPar.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
@@ -262,12 +262,6 @@ 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
@@ -299,12 +293,6 @@ 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 () :=
@@ -848,6 +836,12 @@ 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 ***********************)
@@ -1446,14 +1440,6 @@ 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.
@@ -1524,70 +1510,10 @@ 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 :=
@@ -1676,17 +1602,9 @@ 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 ->
@@ -1768,40 +1686,6 @@ 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.
@@ -1837,14 +1721,6 @@ 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.
@@ -1900,22 +1776,6 @@ 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.
@@ -2247,12 +2107,6 @@ 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.
 
@@ -2326,17 +2180,6 @@ 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.
@@ -2345,34 +2188,12 @@ 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.
@@ -2403,14 +2224,6 @@ 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.
@@ -2419,116 +2232,6 @@ 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.
 
 
@@ -2682,17 +2385,6 @@ 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 b11dded..8dd87da 100644
--- a/theories/soundness.v
+++ b/theories/soundness.v
@@ -10,6 +10,3 @@ 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.