Commit 36f40743 authored by jihgfee's avatar jihgfee

Added some laters in premises

parent 48f38558
Pipeline #25913 passed with stage
in 16 minutes and 59 seconds
......@@ -131,7 +131,7 @@ Section channel.
Global Instance iProto_mapsto_proper c : Proper (() ==> ()) (iProto_mapsto c).
Proof. apply (ne_proper _). Qed.
Lemma iProto_mapsto_le c p1 p2 : c p1 - iProto_le p1 p2 - c p2.
Lemma iProto_mapsto_le c p1 p2 : c p1 - iProto_le p1 p2 - c p2.
Proof.
rewrite iProto_mapsto_eq. iDestruct 1 as (γ s l r lk ->) "[Hlk H]".
iIntros "Hle'". iExists γ, s, l, r, lk. iSplit; [done|]. iFrame "Hlk".
......
......@@ -867,7 +867,7 @@ Section proto.
Proof. apply (ne_proper _). Qed.
Lemma iProto_own_le γ s p1 p2 :
iProto_own γ s p1 - iProto_le p1 p2 - iProto_own γ s p2.
iProto_own γ s p1 - iProto_le p1 p2 - iProto_own γ s p2.
Proof.
iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
......
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