Skip to content
GitLab
Explore
Sign in
Iris
Iris
Issues
#157
`done` loops in proofmode
Lemma
test
:
∃
R
,
R
⊢
∀
P
,
P
.
Proof
.
eexists
.
iIntros
"?"
(
P
)
.
done
.