Commit 0f5eca67 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso

Test new hint for `bi_wand` (from !331)

parent 21bf312c
......@@ -6,6 +6,12 @@ Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma test_eauto_emp_isplit_biwand P : emp P - P.
Proof. eauto 6. Qed.
Lemma test_eauto_isplit_biwand P : (P - P)%I.
Proof. iStartProof. eauto. Qed.
Check "demo_0".
Lemma demo_0 P Q : (P Q) - ( x, x = 0 x = 1) (Q P).
Proof.
......
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