diff --git a/theories/common.v b/theories/common.v
index 9c6b508..3ea15d6 100644
--- a/theories/common.v
+++ b/theories/common.v
@@ -1,4 +1,7 @@
 Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect.
+From Equations Require Import Equations.
+Derive NoConfusion for nat PTag BTag PTm.
+Derive EqDec for BTag PTag PTm.
 From Ltac2 Require Ltac2.
 Import Ltac2.Notations.
 Import Ltac2.Control.
@@ -169,4 +172,6 @@ Module HRed.
   | IndCong P a0 a1 b c :
     R a0 a1 ->
     R (PInd P a0 b c) (PInd P a1 b c).
+
+    Definition nf a := forall b, ~ R a b.
 End HRed.
diff --git a/theories/executable.v b/theories/executable.v
index f773fa6..5de3355 100644
--- a/theories/executable.v
+++ b/theories/executable.v
@@ -1,58 +1,145 @@
 From Equations Require Import Equations.
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax
-  common typing preservation admissible fp_red structural soundness.
-Require Import algorithmic.
-From stdpp Require Import relations (rtc(..), nsteps(..)).
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
 Require Import ssreflect ssrbool.
+Import Logic (inspect).
 
-Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
+Require Import ssreflect ssrbool.
+From Hammer Require Import Tactics.
+
+Definition tm_nonconf (a b : PTm) : bool :=
+  match a, b with
+  | PAbs _, _ => ishne b || isabs b
+  | _, PAbs _ => ishne a
+  | VarPTm _, VarPTm _ => true
+  | PPair _ _, _ => ishne b || ispair b
+  | _, PPair _ _ => ishne a
+  | PZero, PZero => true
+  | PSuc _, PSuc _ => true
+  | PApp _ _, PApp _ _ => ishne a && ishne b
+  | PProj _ _, PProj _ _ => ishne a && ishne b
+  | PInd _ _ _ _, PInd _ _ _ _ => ishne a && ishne b
+  | PNat, PNat => true
+  | PUniv _, PUniv _ => true
+  | PBind _ _ _, PBind _ _ _ => true
+  | _,_=> false
+  end.
+
+Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b.
+
+Inductive eq_view : PTm -> PTm -> Type :=
+| V_AbsAbs a b :
+  eq_view (PAbs a) (PAbs b)
+| V_AbsNeu a b :
+  ~~ isabs b ->
+  eq_view (PAbs a) b
+| V_NeuAbs a b :
+  ~~ isabs a ->
+  eq_view a (PAbs b)
+| V_VarVar i j :
+  eq_view (VarPTm i) (VarPTm j)
+| V_PairPair a0 b0 a1 b1 :
+  eq_view (PPair a0 b0) (PPair a1 b1)
+| V_PairNeu a0 b0 u :
+  ~~ ispair u ->
+  eq_view (PPair a0 b0) u
+| V_NeuPair u a1 b1 :
+  ~~ ispair u ->
+  eq_view u (PPair a1 b1)
+| V_ZeroZero :
+  eq_view PZero PZero
+| V_SucSuc a b :
+  eq_view (PSuc a) (PSuc b)
+| V_AppApp u0 b0 u1 b1 :
+  eq_view (PApp u0 b0) (PApp u1 b1)
+| V_ProjProj p0 u0 p1 u1 :
+  eq_view (PProj p0 u0) (PProj p1 u1)
+| V_IndInd P0 u0 b0 c0  P1 u1 b1 c1 :
+  eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
+| V_NatNat :
+  eq_view PNat PNat
+| V_BindBind p0 A0 B0 p1 A1 B1 :
+  eq_view (PBind p0 A0 B0) (PBind p1 A1 B1)
+| V_UnivUniv i j :
+  eq_view (PUniv i) (PUniv j)
+| V_Others a b :
+  eq_view a b.
+
+Equations tm_to_eq_view (a b : PTm) : eq_view a b :=
+  tm_to_eq_view (PAbs a) (PAbs b) := V_AbsAbs a b;
+  tm_to_eq_view (PAbs a) b := V_AbsNeu a b _;
+  tm_to_eq_view a (PAbs b) := V_NeuAbs a b _;
+  tm_to_eq_view (VarPTm i) (VarPTm j) := V_VarVar i j;
+  tm_to_eq_view (PPair a0 b0) (PPair a1 b1) := V_PairPair a0 b0 a1 b1;
+  tm_to_eq_view (PPair a0 b0) u := V_PairNeu a0 b0 u _;
+  tm_to_eq_view u (PPair a1 b1) := V_NeuPair u a1 b1 _;
+  tm_to_eq_view PZero PZero := V_ZeroZero;
+  tm_to_eq_view (PSuc a) (PSuc b) := V_SucSuc a b;
+  tm_to_eq_view (PApp a0 b0) (PApp a1 b1) := V_AppApp a0 b0 a1 b1;
+  tm_to_eq_view (PProj p0 b0) (PProj p1 b1) := V_ProjProj p0 b0 p1 b1;
+  tm_to_eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) := V_IndInd P0 u0 b0 c0 P1 u1 b1 c1;
+  tm_to_eq_view PNat PNat := V_NatNat;
+  tm_to_eq_view (PUniv i) (PUniv j) := V_UnivUniv i j;
+  tm_to_eq_view (PBind p0 A0 B0)  (PBind p1 A1 B1) := V_BindBind p0 A0 B0 p1 A1 B1;
+  tm_to_eq_view a b := V_Others a b.
+
+Inductive algo_dom : PTm -> PTm -> Prop :=
 | A_AbsAbs a b :
-  algo_dom a b ->
+  algo_dom_r a b ->
   (* --------------------- *)
   algo_dom (PAbs a) (PAbs b)
 
 | A_AbsNeu a u :
   ishne u ->
-  algo_dom a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
+  algo_dom_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
   (* --------------------- *)
   algo_dom (PAbs a) u
 
 | A_NeuAbs a u :
   ishne u ->
-  algo_dom (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
+  algo_dom_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
   (* --------------------- *)
   algo_dom u (PAbs a)
 
 | A_PairPair a0 a1 b0 b1 :
-  algo_dom a0 a1 ->
-  algo_dom b0 b1 ->
+  algo_dom_r a0 a1 ->
+  algo_dom_r b0 b1 ->
   (* ---------------------------- *)
   algo_dom (PPair a0 b0) (PPair a1 b1)
 
 | A_PairNeu a0 a1 u :
   ishne u ->
-  algo_dom a0 (PProj PL u) ->
-  algo_dom a1 (PProj PR u) ->
+  algo_dom_r a0 (PProj PL u) ->
+  algo_dom_r a1 (PProj PR u) ->
   (* ----------------------- *)
   algo_dom (PPair a0 a1) u
 
 | A_NeuPair a0 a1 u :
   ishne u ->
-  algo_dom (PProj PL u) a0 ->
-  algo_dom (PProj PR u) a1 ->
+  algo_dom_r (PProj PL u) a0 ->
+  algo_dom_r (PProj PR u) a1 ->
   (* ----------------------- *)
   algo_dom u (PPair a0 a1)
 
+| A_ZeroZero :
+  algo_dom PZero PZero
+
+| A_SucSuc a0 a1 :
+  algo_dom_r a0 a1 ->
+  algo_dom (PSuc a0) (PSuc a1)
+
 | A_UnivCong i j :
   (* -------------------------- *)
   algo_dom (PUniv i) (PUniv j)
 
 | A_BindCong p0 p1 A0 A1 B0 B1 :
-  algo_dom A0 A1 ->
-  algo_dom B0 B1 ->
+  algo_dom_r A0 A1 ->
+  algo_dom_r B0 B1 ->
   (* ---------------------------- *)
   algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1)
 
+| A_NatCong :
+  algo_dom PNat PNat
+
 | A_VarCong i j :
   (* -------------------------- *)
   algo_dom (VarPTm i) (VarPTm j)
@@ -68,78 +155,197 @@ Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
   ishne u0 ->
   ishne u1 ->
   algo_dom u0 u1 ->
-  algo_dom a0 a1 ->
+  algo_dom_r a0 a1 ->
   (* ------------------------- *)
   algo_dom (PApp u0 a0) (PApp u1 a1)
 
+| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 :
+  ishne u0 ->
+  ishne u1 ->
+  algo_dom_r P0 P1 ->
+  algo_dom u0 u1 ->
+  algo_dom_r b0 b1 ->
+  algo_dom_r c0 c1 ->
+  algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
+
+with algo_dom_r : PTm  -> PTm -> Prop :=
+| A_NfNf a b :
+  algo_dom a b ->
+  algo_dom_r a b
+
 | A_HRedL a a' b  :
   HRed.R a a' ->
-  algo_dom a' b ->
+  algo_dom_r a' b ->
   (* ----------------------- *)
-  algo_dom a b
+  algo_dom_r a b
 
 | A_HRedR a b b'  :
   ishne a \/ ishf a ->
   HRed.R b b' ->
-  algo_dom a b' ->
+  algo_dom_r a b' ->
   (* ----------------------- *)
-  algo_dom a b.
+  algo_dom_r a b.
 
-
-Definition fin_eq {n} (i j : fin n) : bool.
+Lemma algo_dom_hf_hne (a b : PTm) :
+  algo_dom a b ->
+  (ishf a \/ ishne a) /\ (ishf b \/ ishne b).
 Proof.
-  induction n.
-  - by exfalso.
-  - refine (match i , j with
-            | None, None => true
-            | Some i, Some j => IHn i j
-            | _, _ => false
-            end).
+  induction 1 =>//=; hauto lq:on.
+Qed.
+
+Lemma hf_no_hred (a b : PTm) :
+  ishf a ->
+  HRed.R a b ->
+  False.
+Proof. hauto l:on inv:HRed.R. Qed.
+
+Lemma hne_no_hred (a b : PTm) :
+  ishne a ->
+  HRed.R a b ->
+  False.
+Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed.
+
+Derive Signature for algo_dom algo_dom_r.
+
+Fixpoint hred (a : PTm) : option (PTm) :=
+    match a with
+    | VarPTm i => None
+    | PAbs a => None
+    | PApp (PAbs a) b => Some (subst_PTm (scons b VarPTm) a)
+    | PApp a b =>
+        match hred a with
+        | Some a => Some (PApp a b)
+        | None => None
+        end
+    | PPair a b => None
+    | PProj p (PPair a b) => if p is PL then Some a else Some b
+    | PProj p a =>
+        match hred a with
+        | Some a => Some (PProj p a)
+        | None => None
+        end
+    | PUniv i => None
+    | PBind p A B => None
+    | PNat => None
+    | PZero => None
+    | PSuc a => None
+    | PInd P PZero b c => Some b
+    | PInd P (PSuc a) b c =>
+        Some (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
+    | PInd P a b c =>
+        match hred a with
+        | Some a => Some (PInd P a b c)
+        | None => None
+        end
+    end.
+
+Lemma hred_complete (a b : PTm) :
+  HRed.R a b -> hred a = Some b.
+Proof.
+  induction 1; hauto lq:on rew:off inv:HRed.R b:on.
+Qed.
+
+Lemma hred_sound (a b : PTm):
+  hred a = Some b -> HRed.R a b.
+Proof.
+  elim : a b; hauto q:on dep:on ctrs:HRed.R.
+Qed.
+
+Lemma hred_deter (a b0 b1 : PTm) :
+  HRed.R a b0 -> HRed.R a b1 -> b0 = b1.
+Proof.
+  move /hred_complete => + /hred_complete. congruence.
+Qed.
+
+Definition fancy_hred (a : PTm) : HRed.nf a + {b | HRed.R a b}.
+  destruct (hred a) eqn:eq.
+  right. exists p. by apply hred_sound in eq.
+  left. move => b /hred_complete. congruence.
 Defined.
 
-Lemma fin_eq_dec {n} (i j : fin n) :
-  Bool.reflect (i = j) (fin_eq i j).
-Proof.
-  revert i j. induction n.
-  - destruct i.
-  - destruct i; destruct j.
-    + specialize (IHn f f0).
-      inversion IHn; subst.
-      simpl. rewrite -H.
-      apply ReflectT.
-      reflexivity.
-      simpl. rewrite -H.
-      apply ReflectF.
-      injection. tauto.
-    + by apply ReflectF.
-    + by apply ReflectF.
-    + by apply ReflectT.
-Defined.
+Ltac check_equal_triv :=
+  intros;subst;
+  lazymatch goal with
+  (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
+  | [h : algo_dom _ _ |- _] => try (inversion h; by subst)
+  | _ => idtac
+  end.
 
+Ltac solve_check_equal :=
+  try solve [intros *;
+  match goal with
+  | [|- _ = _] => sauto
+  | _ => idtac
+  end].
 
-Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) :
+Equations check_equal (a b : PTm) (h : algo_dom a b) :
   bool by struct h :=
-  check_equal a b h with (@idP (ishne a || ishf a)) := {
-    | Bool.ReflectT _ _ => _
-    | Bool.ReflectF _ _ => _
-    }.
+  check_equal a b h with tm_to_eq_view a b :=
+  check_equal _ _ h (V_VarVar i j) := nat_eqdec i j;
+  check_equal _ _ h (V_AbsAbs a b) := check_equal_r a b ltac:(check_equal_triv);
+  check_equal _ _ h (V_AbsNeu a b h') := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv);
+  check_equal _ _ h (V_NeuAbs a b _) := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv);
+  check_equal _ _ h (V_PairPair a0 b0 a1 b1) :=
+    check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv);
+  check_equal _ _ h (V_PairNeu a0 b0 u _) :=
+    check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv);
+  check_equal _ _ h (V_NeuPair u a1 b1 _) :=
+    check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv);
+  check_equal _ _ h V_NatNat := true;
+  check_equal _ _ h V_ZeroZero := true;
+  check_equal _ _ h (V_SucSuc a b) := check_equal_r a b ltac:(check_equal_triv);
+  check_equal _ _ h (V_ProjProj p0 a p1 b) :=
+    PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv);
+  check_equal _ _ h (V_AppApp a0 b0 a1 b1) :=
+    check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv);
+  check_equal _ _ h (V_IndInd P0 u0 b0 c0 P1 u1 b1 c1) :=
+    check_equal_r P0 P1 ltac:(check_equal_triv) &&
+      check_equal u0 u1 ltac:(check_equal_triv) &&
+      check_equal_r b0 b1 ltac:(check_equal_triv) &&
+      check_equal_r c0 c1 ltac:(check_equal_triv);
+  check_equal _ _ h (V_UnivUniv i j) := nat_eqdec i j;
+  check_equal _ _ h (V_BindBind p0 A0 B0 p1 A1 B1) :=
+    BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv);
+  check_equal _ _ _ _ := false
 
+  (* check_equal a b h := false; *)
+  with check_equal_r (a b : PTm) (h0 : algo_dom_r a b) :
+  bool by struct h0 :=
+    check_equal_r a b h with (fancy_hred a) :=
+      check_equal_r a b h (inr a') := check_equal_r (proj1_sig a') b _;
+      check_equal_r a b h (inl h')  with (fancy_hred b) :=
+        | inr b' := check_equal_r a (proj1_sig b') _;
+        | inl h'' := check_equal a b _.
 
-  (* check_equal (VarPTm i) (VarPTm j) h := fin_eq i j; *)
-  (* check_equal (PAbs a) (PAbs b) h := check_equal a b _; *)
-  (* check_equal (PPair a0 b0) (PPair a1 b1) h := *)
-  (*   check_equal a0 b0 _ && check_equal a1 b1 _; *)
-  (* check_equal (PUniv i) (PUniv j) _ := _; *)
 Next Obligation.
-  simpl.
-  intros ih.
-Admitted.
+  intros.
+  inversion h; subst => //=.
+  exfalso. hauto l:on use:hred_complete unfold:HRed.nf.
+  exfalso. hauto l:on use:hred_complete unfold:HRed.nf.
+Defined.
 
-Search (Bool.reflect (is_true _) _).
-Check idP.
+Next Obligation.
+  intros.
+  destruct h.
+  exfalso. apply algo_dom_hf_hne in H0.
+  destruct H0 as [h0 h1].
+  sfirstorder use:hf_no_hred, hne_no_hred.
+  exfalso. sfirstorder.
+  assert (  b' = b'0)by eauto using hred_deter. subst.
+  apply h.
+Defined.
 
-Definition 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 /\ size_PTm va + size_PTm vb + i + j <= k.
+Next Obligation.
+  simpl. intros.
+  inversion h; subst =>//=.
+  move {h}. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred, hred_sound.
+  assert (a' = a'0) by eauto using hred_deter, hred_sound. by subst.
+  exfalso. sfirstorder use:hne_no_hred, hf_no_hred.
+Defined.
 
-Search (nat -> nat -> bool).
+
+
+
+Next Obligation.
+  qauto inv:algo_dom, algo_dom_r.
+Defined.
diff --git a/theories/executable_correct.v b/theories/executable_correct.v
new file mode 100644
index 0000000..603c91c
--- /dev/null
+++ b/theories/executable_correct.v
@@ -0,0 +1,162 @@
+From Equations Require Import Equations.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common executable algorithmic.
+Require Import ssreflect ssrbool.
+From stdpp Require Import relations (rtc(..)).
+From Hammer Require Import Tactics.
+
+Scheme algo_ind := Induction for algo_dom Sort Prop
+  with algor_ind := Induction for algo_dom_r Sort Prop.
+
+Combined Scheme algo_dom_mutual from algo_ind, algor_ind.
+
+Lemma check_equal_pair_neu a0 a1 u neu h h'
+  : check_equal (PPair a0 a1) u (A_PairNeu a0 a1 u neu h h') = check_equal_r a0 (PProj PL u) h && check_equal_r a1 (PProj PR u) h'.
+Proof.
+  case : u neu h h' => //=; simp check_equal tm_to_eq_view.
+Qed.
+
+Lemma check_equal_neu_pair a0 a1 u neu h h'
+  : check_equal u (PPair a0 a1) (A_NeuPair a0 a1 u neu h h') = check_equal_r  (PProj PL u) a0 h && check_equal_r (PProj PR u) a1 h'.
+Proof.
+  case : u neu h h' => //=; simp check_equal tm_to_eq_view.
+Qed.
+
+Lemma check_equal_bind_bind p0 A0 B0 p1 A1 B1 h0 h1 :
+  check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) (A_BindCong p0 p1 A0 A1 B0 B1 h0 h1) =
+    BTag_eqdec p0 p1 &&  check_equal_r A0 A1 h0 && check_equal_r  B0 B1 h1.
+Proof. hauto lq:on. Qed.
+
+Lemma check_equal_proj_proj p0 u0 p1 u1 neu0 neu1 h :
+  check_equal (PProj p0 u0) (PProj p1 u1) (A_ProjCong p0 p1 u0 u1 neu0 neu1 h) =
+    PTag_eqdec p0 p1 && check_equal u0 u1 h.
+Proof. hauto lq:on. Qed.
+
+Lemma check_equal_app_app u0 a0 u1 a1 hu0 hu1 hdom hdom' :
+  check_equal (PApp u0 a0) (PApp u1 a1) (A_AppCong u0 u1 a0 a1 hu0 hu1 hdom hdom') =
+    check_equal u0 u1 hdom && check_equal_r a0 a1 hdom'.
+Proof. hauto lq:on. Qed.
+
+Lemma check_equal_ind_ind P0 u0 b0 c0 P1 u1 b1 c1 neu0 neu1 domP domu domb domc :
+  check_equal (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
+    (A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP domu domb domc) =
+    check_equal_r P0 P1 domP && check_equal u0 u1 domu && check_equal_r b0 b1 domb && check_equal_r c0 c1 domc.
+Proof. hauto lq:on. Qed.
+
+Lemma hred_none a : HRed.nf a -> hred a = None.
+Proof.
+  destruct (hred a) eqn:eq;
+  sfirstorder use:hred_complete, hred_sound.
+Qed.
+
+Lemma check_equal_nfnf a b dom : check_equal_r a b (A_NfNf a b dom) = check_equal a b dom.
+Proof.
+  have [h0 h1] : (ishf a \/ ishne a) /\ (ishf b \/ ishne b) by hauto l:on use:algo_dom_hf_hne.
+  have [h3 h4] : hred a = None /\ hred b = None by sfirstorder use:hf_no_hred, hne_no_hred, hred_none.
+  simp check_equal.
+  destruct (fancy_hred a).
+  simp check_equal.
+  destruct (fancy_hred b).
+  simp check_equal. hauto lq:on.
+  exfalso. hauto l:on use:hred_complete.
+  exfalso. hauto l:on use:hred_complete.
+Qed.
+
+Lemma check_equal_hredl a b a' ha doma :
+  check_equal_r a b (A_HRedL a a' b ha doma) = check_equal_r a' b doma.
+Proof.
+  simp check_equal.
+  destruct (fancy_hred a).
+  - hauto q:on unfold:HRed.nf.
+  - simp check_equal.
+    destruct s as [x ?]. have ? : x = a' by eauto using hred_deter. subst.
+    simpl.
+    simp check_equal.
+    f_equal.
+    apply PropExtensionality.proof_irrelevance.
+Qed.
+
+Lemma check_equal_hredr a b b' hu r a0 :
+  check_equal_r a b (A_HRedR a b b' hu r a0) =
+    check_equal_r a b' a0.
+Proof.
+  simp check_equal.
+  destruct (fancy_hred a).
+  - rewrite check_equal_r_clause_1_equation_1.
+    destruct (fancy_hred b) as [|[b'' hb']].
+    + hauto lq:on unfold:HRed.nf.
+    + have ? : (b'' = b') by eauto using hred_deter. subst.
+      rewrite check_equal_r_clause_1_equation_1.  simpl.
+      simp check_equal. destruct (fancy_hred a). simp check_equal.
+      f_equal; apply PropExtensionality.proof_irrelevance.
+      simp check_equal. exfalso. sfirstorder use:hne_no_hred, hf_no_hred.
+  - simp check_equal. exfalso.
+    sfirstorder use:hne_no_hred, hf_no_hred.
+Qed.
+
+Lemma coqeq_neuneu u0 u1 :
+  ishne u0 -> ishne u1 -> u0 ↔ u1 -> u0 ∼ u1.
+Proof.
+  inversion 3; subst => //=.
+Qed.
+
+Lemma check_equal_sound :
+  (forall a b (h : algo_dom a b), check_equal a b h -> a ↔ b) /\
+  (forall a b (h : algo_dom_r a b), check_equal_r a b h -> a ⇔ b).
+Proof.
+  apply algo_dom_mutual.
+  - move => a b h.
+    move => h0 h1.
+    have {}h1 : check_equal_r a b h by hauto l:on rew:db:check_equal.
+    constructor. tauto.
+  - move => a u i h0 ih h.
+    apply CE_AbsNeu => //.
+    apply : ih. simp check_equal tm_to_eq_view in h.
+    have h1 : check_equal (PAbs a) u (A_AbsNeu a u i h0) = check_equal_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) h0 by  clear; case : u i h0 => //=.
+    hauto lq:on.
+  - move => a u i h ih h0.
+    apply CE_NeuAbs=>//.
+    apply ih.
+    case : u i h ih h0 => //=.
+  - move => a0 a1 b0 b1 a ha h.
+    move => h0 h1. constructor. apply ha. hauto lb:on rew:db:check_equal.
+    apply h0. hauto lb:on rew:db:check_equal.
+  - move => a0 a1 u neu h ih h' ih' he.
+    rewrite check_equal_pair_neu in he.
+    apply CE_PairNeu => //; hauto lqb:on.
+  - move => a0 a1 u i a ha a2 hb.
+    rewrite check_equal_neu_pair => *.
+    apply CE_NeuPair => //; hauto lqb:on.
+  - sfirstorder.
+  - hauto l:on use:CE_SucSuc.
+  - move => i j /sumboolP.
+    hauto lq:on use:CE_UnivCong.
+  - move => p0 p1 A0 A1 B0 B1 h0 ih0 h1 ih1 h2.
+    rewrite check_equal_bind_bind in h2.
+    move : h2.
+    move /andP => [/andP [h20 h21] h3].
+    move /sumboolP : h20 => ?. subst.
+    hauto l:on use:CE_BindCong.
+  - sfirstorder.
+  - move => i j /sumboolP ?.  subst.
+    apply : CE_NeuNeu. apply CE_VarCong.
+  - move => p0 p1 u0 u1 neu0 neu1 h ih he.
+    apply CE_NeuNeu.
+    rewrite check_equal_proj_proj in he.
+    move /andP : he => [/sumboolP ? h1]. subst.
+    sauto lq:on use:coqeq_neuneu.
+  - move => u0 u1 a0 a1 hu0 hu1 hdom ih hdom' ih' hE.
+    rewrite check_equal_app_app in hE.
+    move /andP : hE => [h0 h1].
+    sauto lq:on use:coqeq_neuneu.
+  - move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc.
+    rewrite check_equal_ind_ind.
+    move /andP => [/andP [/andP [h0 h1] h2 ] h3].
+    sauto lq:on use:coqeq_neuneu.
+  - move => a b dom h ih. apply : CE_HRed; eauto using rtc_refl.
+    rewrite check_equal_nfnf in ih.
+    tauto.
+  - move => a a' b ha doma ih hE.
+    rewrite check_equal_hredl in hE. sauto lq:on.
+  - move => a b b' hu r a0 ha hb. rewrite check_equal_hredr in hb.
+    sauto lq:on rew:off.
+Qed.