Verified Commit fc5c9162 authored by Tej Chajed's avatar Tej Chajed

Remove exists example for now

parent 4e574119
......@@ -20,14 +20,6 @@ Proof.
iPureIntro.
exact (Himpl HP2).
Qed.
Lemma exists_demo P1 (P2: nat -> PROP) :
P1 ( x, P2 x) - x, P1 P2 x.
Proof.
iIntros "[? [%x HP2]]".
iFrame.
iExists x; iExact "HP2".
Qed.
```
## Acknowledgements
......
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