Commit 74639a53 authored by Robbert Krebbers's avatar Robbert Krebbers

New lemma `Next_uninj x : ∃ a, x ≡ Next a`.

This lemma allows one to get the witness out of a later, without having
to use `later_car`, i.e. in a way that works in the on-paper version of
the logic.
parent b1d87589
......@@ -1022,6 +1022,8 @@ Section later.
Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
Proof. by intros x y. Qed.
Lemma Next_uninj x : a, x Next a.
Proof. by exists (later_car x). Qed.
Instance later_car_anti_contractive n :
Proper (dist n ==> dist_later n) later_car.
Proof. move=> [x] [y] /= Hxy. done. 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