Commit 733ab29a authored by Robbert's avatar Robbert

Merge branch 'nsteps_inv' into 'master'

relations.nsteps: add inversion lemma for `nsteps R 1 a b`

See merge request !87
parents 0b3d1e9f dfe225f7
...@@ -137,6 +137,8 @@ Section closure. ...@@ -137,6 +137,8 @@ Section closure.
Lemma nsteps_once x y : R x y nsteps R 1 x y. Lemma nsteps_once x y : R x y nsteps R 1 x y.
Proof. eauto. Qed. Proof. eauto. Qed.
Lemma nsteps_once_inv x y : nsteps R 1 x y R x y.
Proof. inversion 1 as [|???? Hhead Htail]; inversion Htail; by subst. Qed.
Lemma nsteps_trans n m x y z : Lemma nsteps_trans n m x y z :
nsteps R n x y nsteps R m y z nsteps R (n + m) x z. nsteps R n x y nsteps R m y z nsteps R (n + m) x z.
Proof. induction 1; simpl; eauto. Qed. Proof. induction 1; simpl; eauto. Qed.
......
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