From 00865060ae43744b9d6e44d1a99c995f7c15b090 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 9 Nov 2020 14:27:40 +0100
Subject: [PATCH] cleanup

---
 theories/logic/spec_rules.v | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 2d79d34..e8d0dbf 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 :
-- 
GitLab