Commit 8f725f45 authored by Ralf Jung's avatar Ralf Jung
Browse files

use Lemma, not Let

parent 46cc91ed
......@@ -115,7 +115,7 @@ Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
P - Q R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
Let test_fresh P Q:
Lemma test_fresh P Q:
(P Q) - (P Q).
iIntros "H".
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