Skip to content
Snippets Groups Projects
Commit 777d9fe1 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove more useless laters.

parent 8957c470
No related branches found
No related tags found
No related merge requests found
Pipeline #24289 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/channel/proto_channel.v
+ 3
− 3
View file @ 777d9fe1
...@@ -597,9 +597,9 @@ Section proto. ...@@ -597,9 +597,9 @@ Section proto.
Qed. Qed.
Lemma proto_interp_recv v vs p1 pc : Lemma proto_interp_recv v vs p1 pc :
proto_interp (v :: vs) p1 (proto_message Receive pc) -∗ ∃ p2, proto_interp (v :: vs) p1 (proto_message Receive pc) -∗ ∃ p2,
pc v (proto_eq_next p2) ∗ pc v (proto_eq_next p2) ∗
▷ proto_interp vs p1 p2. proto_interp vs p1 p2.
Proof. Proof.
simpl. iDestruct 1 as (pc' p2) "(Heq & Hc & Hp2)". iExists p2. iFrame "Hp2". simpl. iDestruct 1 as (pc' p2) "(Heq & Hc & Hp2)". iExists p2. iFrame "Hp2".
iDestruct (@proto_message_equivI with "Heq") as "[_ Heq]". iDestruct (@proto_message_equivI with "Heq") as "[_ Heq]".
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment