Skip to content

GitLab

Closed
Created by Robbert Krebbers@robbertkrebbersMaintainer

`done` loops in proofmode

Lemma test : ∃ R, R ⊢ ∀ P, P.
Proof. eexists. iIntros "?" (P). done.