diff --git a/theories/fp_red.v b/theories/fp_red.v
index cb3bdb4..4b6f624 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -105,58 +105,6 @@ Module ERed.
 
 End ERed.
 
-Module NeERed.
-  Inductive R_nonelim {n} : PTm n -> PTm n ->  Prop :=
-  (****************** Eta ***********************)
-  | AppEta A a0 a1 :
-    R_nonelim a0 a1 ->
-    R_nonelim (PAbs A (PApp (ren_PTm shift a0) (VarPTm var_zero))) a1
-  | PairEta a0 a1 :
-    R_nonelim a0 a1 ->
-    R_nonelim (PPair (PProj PL a0) (PProj PR a0)) a1
-  (*************** Congruence ********************)
-  | AbsCong A a0 a1 :
-    R_nonelim a0 a1 ->
-    R_nonelim (PAbs A a0) (PAbs A a1)
-  | AppCong a0 a1 b0 b1 :
-    R_elim a0 a1 ->
-    R_nonelim b0 b1 ->
-    R_nonelim (PApp a0 b0) (PApp a1 b1)
-  | PairCong a0 a1 b0 b1 :
-    R_nonelim a0 a1 ->
-    R_nonelim b0 b1 ->
-    R_nonelim (PPair a0 b0) (PPair a1 b1)
-  | ProjCong p a0 a1 :
-    R_elim a0 a1 ->
-    R_nonelim (PProj p a0) (PProj p a1)
-  | VarTm i :
-    R_nonelim (VarPTm i) (VarPTm i)
-  with R_elim {n} : PTm n -> PTm n -> Prop :=
-  | NAbsCong A a0 a1 :
-    R_nonelim a0 a1 ->
-    R_elim (PAbs A a0) (PAbs A a1)
-  | NAppCong a0 a1 b0 b1 :
-    R_elim a0 a1 ->
-    R_nonelim b0 b1 ->
-    R_elim (PApp a0 b0) (PApp a1 b1)
-  | NPairCong a0 a1 b0 b1 :
-    R_nonelim a0 a1 ->
-    R_nonelim b0 b1 ->
-    R_elim (PPair a0 b0) (PPair a1 b1)
-  | NProjCong p a0 a1 :
-    R_elim a0 a1 ->
-    R_elim (PProj p a0) (PProj p a1)
-  | NVarTm i :
-    R_elim (VarPTm i) (VarPTm i).
-
-  Scheme ered_elim_ind := Induction for R_elim Sort Prop
-      with ered_nonelim_ind := Induction for R_nonelim Sort Prop.
-
-  Combined Scheme ered_mutual from ered_elim_ind, ered_nonelim_ind.
-
-
-End NeERed.
-
 Inductive SNe {n} : PTm n -> Prop :=
 | N_Var i :
   SNe (VarPTm i)
@@ -564,6 +512,96 @@ Proof.
   elim : n a b /h=>//=; hauto qb:on use:ne_nf_ren, ne_nf.
 Qed.
 
+Definition ishf {n} (a : PTm n) :=
+  match a with
+  | PPair _ _ => true
+  | PAbs _ => true
+  | _ => false
+  end.
+
+Module NeERed.
+  Inductive R_nonelim {n} : PTm n -> PTm n ->  Prop :=
+  (****************** Eta ***********************)
+  | AppEta a0 a1 :
+    ~~ ishf a0 ->
+    R_elim a0 a1 ->
+    R_nonelim (PAbs (PApp (ren_PTm shift a0) (VarPTm var_zero))) a1
+  | PairEta a0 a1 :
+    ~~ ishf a0 ->
+    R_elim a0 a1 ->
+    R_nonelim (PPair (PProj PL a0) (PProj PR a0)) a1
+  (*************** Congruence ********************)
+  | AbsCong a0 a1 :
+    R_nonelim a0 a1 ->
+    R_nonelim (PAbs a0) (PAbs a1)
+  | AppCong a0 a1 b0 b1 :
+    R_elim a0 a1 ->
+    R_nonelim b0 b1 ->
+    R_nonelim (PApp a0 b0) (PApp a1 b1)
+  | PairCong a0 a1 b0 b1 :
+    R_nonelim a0 a1 ->
+    R_nonelim b0 b1 ->
+    R_nonelim (PPair a0 b0) (PPair a1 b1)
+  | ProjCong p a0 a1 :
+    R_elim a0 a1 ->
+    R_nonelim (PProj p a0) (PProj p a1)
+  | VarTm i :
+    R_nonelim (VarPTm i) (VarPTm i)
+  with R_elim {n} : PTm n -> PTm n -> Prop :=
+  | NAbsCong a0 a1 :
+    R_nonelim a0 a1 ->
+    R_elim (PAbs a0) (PAbs a1)
+  | NAppCong a0 a1 b0 b1 :
+    R_elim a0 a1 ->
+    R_nonelim b0 b1 ->
+    R_elim (PApp a0 b0) (PApp a1 b1)
+  | NPairCong a0 a1 b0 b1 :
+    R_nonelim a0 a1 ->
+    R_nonelim b0 b1 ->
+    R_elim (PPair a0 b0) (PPair a1 b1)
+  | NProjCong p a0 a1 :
+    R_elim a0 a1 ->
+    R_elim (PProj p a0) (PProj p a1)
+  | NVarTm i :
+    R_elim (VarPTm i) (VarPTm i).
+
+  Scheme ered_elim_ind := Induction for R_elim Sort Prop
+      with ered_nonelim_ind := Induction for R_nonelim Sort Prop.
+
+  Combined Scheme ered_mutual from ered_elim_ind, ered_nonelim_ind.
+
+  Lemma R_elim_nf n :
+    (forall (a b : PTm n), R_elim a b -> nf b -> nf a) /\
+      (forall (a b : PTm n), R_nonelim a b -> nf b -> nf a).
+  Proof.
+    move : n. apply ered_mutual => n //=.
+    - move => a0 a1 b0 b1 h ih h' ih' /andP [h0 h1].
+      have hb0 : nf b0 by eauto.
+      suff : ne a0 by qauto b:on.
+      qauto l:on inv:R_elim.
+    - hauto lb:on.
+    - hauto lq:on inv:R_elim.
+    - move => a0 a1 /negP ha' ha ih ha1.
+      have {ih} := ih ha1.
+      move => ha0.
+      suff : ne a0 by hauto lb:on drew:off use:ne_nf_ren.
+      inversion ha; subst => //=.
+    - move => a0 a1 /negP ha' ha ih ha1.
+      have {}ih := ih ha1.
+      have : ne a0 by hauto lq:on inv:PTm.
+      qauto lb:on.
+    - move => a0 a1 b0 b1 ha iha hb ihb /andP [h0 h1].
+      have {}ihb := ihb h1.
+      have {}iha := iha ltac:(eauto using ne_nf).
+      suff : ne a0 by hauto lb:on.
+      move : ha h0. hauto lq:on inv:R_elim.
+    - hauto lb: on drew: off.
+    - hauto lq:on rew:off inv:R_elim.
+  Qed.
+
+
+End NeERed.
+
 Lemma η_nf_to_ne n (a0 a1 : PTm n) :
   ERed'.R a0 a1 -> nf a0 -> ~~ ne a0 -> ne a1 ->
   (a0 = PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) \/