diff --git a/tests/proofmode.v b/tests/proofmode.v
index 85903527afee202cdab0dad918da1d8552b72c69..4a962019ca130bdf8a6449972f773baf9f816caf 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -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.