Commit 5df24900 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove unused lemma.

parent c60ac407
Pipeline #35265 passed with stage
in 27 minutes and 42 seconds
......@@ -29,20 +29,6 @@ Section excl.
Qed.
End excl.
Section heap_extra.
Context `{heapG Σ}.
Lemma bogus_heap p (q1 q2: Qp) a b:
~((q1 + q2)%Qp 1%Qp)%Qc
p {q1} a p {q2} b False.
Proof.
iIntros (?) "Hp".
iDestruct "Hp" as "[Hl Hr]".
iDestruct (@mapsto_valid_2 with "Hl Hr") as %H'. done.
Qed.
End heap_extra.
Section big_op_later.
Context {M : ucmraT}.
Context `{Countable K} {A : Type}.
......
Supports Markdown
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