diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 2d79d34446bba0d49c76bf3305e536c88b3b2ee4..e8d0dbf9fea0b2b26a15886de9eec3bd48207fab 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -39,18 +39,6 @@ Section rules.
     erased_step (tp, σ) (<[j:=fill K e']> tp, σ').
   Proof. rewrite -(right_id_L [] (++) (<[_:=_]>_)). by apply step_insert. Qed.
 
-  Lemma nsteps_inv_r {A} n (R : A → A → Prop) x y :
-    relations.nsteps R (S n) x y → ∃ z, relations.nsteps R n x z ∧ R z y.
-  Proof.
-    revert x y; induction n; intros x y.
-    - inversion 1; subst.
-      match goal with H : relations.nsteps _ 0 _ _ |- _ => inversion H end; subst.
-      eexists; repeat econstructor; eauto.
-    - inversion 1; subst.
-      edestruct IHn as [z [? ?]]; eauto.
-      exists z; split; eauto using relations.nsteps_l.
-  Qed.
-
   (** * Main rules *)
   (** Pure reductions *)
   Lemma step_pure E j K e e' (P : Prop) n :