-
Robbert Krebbers authored
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.
74639a53
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.