Commit e5b6840b authored by Ralf Jung's avatar Ralf Jung

now this should work on 8.10 as well... sigh

parent ace0db94
Pipeline #22773 passed with stage
in 21 minutes and 11 seconds
......@@ -177,15 +177,15 @@ Section cfg.
Proof. rewrite -(right_id_L [] (++) (<[_:=_]>_)). by apply step_insert. Qed.
Lemma nsteps_inv_r {A} n (R : A A Prop) x y :
nsteps R (S n) x y z, nsteps R n x z R z 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 : nsteps _ 0 _ _ |- _ => inversion H end; 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 nsteps_l.
exists z; split; eauto using relations.nsteps_l.
Qed.
Lemma step_pure' E j K e e' (P : Prop) n :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment