diff --git a/theories/fp_red.v b/theories/fp_red.v
index 382f25b..507eb5a 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -719,6 +719,8 @@ Module RRed.
     move => */=; apply : IndSuc'; eauto. by asimpl.
   Qed.
 
+  Lemma abs_preservation a b : isabs a -> R a b -> isabs b. hauto q:on inv:R. Qed.
+
 End RRed.
 
 Module RPar.
@@ -1004,6 +1006,9 @@ Qed.
 
 Module RReds.
 
+  Lemma abs_preservation a b : isabs a -> rtc RRed.R a b -> isabs b.
+    induction 2; hauto lq:on use:RRed.abs_preservation. Qed.
+
   #[local]Ltac solve_s_rec :=
   move => *; eapply rtc_l; eauto;
          hauto lq:on ctrs:RRed.R.
@@ -1755,6 +1760,15 @@ Module ERed.
 
   Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop.
 
+  Lemma abs_back_preservation (a b : PTm) :
+    SN a -> R a b -> isabs b -> isabs a.
+  Proof.
+    move => + h.
+    elim : a b /h => //=.
+    case => //=. move => p. move /SN_NoForbid.P_PairInv.
+    sfirstorder use:SN_NoForbid.PProj_imp.
+  Qed.
+
   Lemma ToEPar (a b : PTm) :
     ERed.R a b -> EPar.R a b.
   Proof.
@@ -3292,7 +3306,6 @@ Module DJoin.
   Qed.
 End DJoin.
 
-
 Module Sub1.
   Inductive R : PTm -> PTm -> Prop :=
   | Refl a :