diff --git a/theories/algorithmic.v b/theories/algorithmic.v
index dff32da..17868a0 100644
--- a/theories/algorithmic.v
+++ b/theories/algorithmic.v
@@ -737,8 +737,6 @@ Lemma A_Conf' a b :
   algo_dom_r a b.
 Proof.
   move => ha hb.
-  have {}ha : HRed.nf a by sfirstorder use:hf_no_hred, hne_no_hred.
-  have {}hb : HRed.nf b by sfirstorder use:hf_no_hred, hne_no_hred.
   move => ?.
   apply A_NfNf.
   by apply A_Conf.
@@ -1234,6 +1232,11 @@ Qed.
 Lemma algo_dom_r_algo_dom : forall a b, HRed.nf a -> HRed.nf b -> algo_dom_r a b -> algo_dom a b.
 Proof. hauto l:on use:algo_dom_r_inv, hreds_nf_refl. Qed.
 
+Lemma algo_dom_algo_dom_neu : forall a b, ishne a -> ishne b -> algo_dom a b -> algo_dom_neu a b \/ tm_conf a b.
+Proof.
+  inversion 3; subst => //=; tauto.
+Qed.
+
 Lemma term_metric_algo_dom : forall k a b, term_metric k a b -> algo_dom_r a b.
 Proof.
   move => [:hneL].
@@ -1268,9 +1271,12 @@ Proof.
     case : b hfa hfb h => //=; case a => //=; eauto 5 using A_Conf' with adom.
     + move => a0 b0 a1 b1 nfa0 nfa1.
       move /term_metric_app /(_ nfa0  nfa1) => [j][hj][ha]hb.
-      apply A_NfNf. apply A_AppCong => //; eauto.
-      have {}nfa0 : HRed.nf a0 by sfirstorder use:hne_no_hred.
-      have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred.
+      apply A_NfNf.
+      (* apply A_NfNf. apply A_NeuNeu. apply A_AppCong => //; eauto. *)
+      have nfa0' : HRed.nf a0 by sfirstorder use:hne_no_hred.
+      have nfb0' : HRed.nf a1 by sfirstorder use:hne_no_hred.
+      have ha0 : algo_dom a0 a1 by eauto using algo_dom_r_algo_dom.
+      apply A_Conf. admit. admit. rewrite /tm_conf. simpl.
       eauto using algo_dom_r_algo_dom.
     + move => p0 A0 p1 A1 neA0 neA1.
       have {}nfa0 : HRed.nf A0 by sfirstorder use:hne_no_hred.
diff --git a/theories/common.v b/theories/common.v
index c14bbb3..b4867d2 100644
--- a/theories/common.v
+++ b/theories/common.v
@@ -129,9 +129,9 @@ Definition tm_nonconf (a b : PTm) : bool :=
   | _, PPair _ _ => ~~ ishf a
   | PZero, PZero => true
   | PSuc _, PSuc _ => true
-  | PApp _ _, PApp _ _ => (~~ ishf a) && (~~ ishf b)
-  | PProj _ _, PProj _ _ => (~~ ishf a) && (~~ ishf b)
-  | PInd _ _ _ _, PInd _ _ _ _ => (~~ ishf a) && (~~ ishf b)
+  | PApp _ _, PApp _ _ => true
+  | PProj _ _, PProj _ _ => true
+  | PInd _ _ _ _, PInd _ _ _ _ => true
   | PNat, PNat => true
   | PUniv _, PUniv _ => true
   | PBind _ _ _, PBind _ _ _ => true
@@ -140,8 +140,6 @@ Definition tm_nonconf (a b : PTm) : bool :=
 
 Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b.
 
-
-
 Definition ishf_ren (a : PTm)  (ξ : nat -> nat) :
   ishf (ren_PTm ξ a) = ishf a.
 Proof. case : a => //=. Qed.
@@ -262,8 +260,8 @@ Inductive algo_dom : PTm -> PTm -> Prop :=
   algo_dom a b
 
 | A_Conf a b :
-  HRed.nf a ->
-  HRed.nf b ->
+  ishf a ->
+  ishf b ->
   tm_conf a b ->
   algo_dom a b
 
@@ -296,6 +294,12 @@ with algo_dom_neu : PTm -> PTm -> Prop :=
   algo_dom_r c0 c1 ->
   algo_dom_neu (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
 
+| A_NeuConf a b :
+  ishne a ->
+  ishne b ->
+  tm_conf a b ->
+  algo_dom_neu a b
+
 with algo_dom_r : PTm  -> PTm -> Prop :=
 | A_NfNf a b :
   algo_dom a b ->