diff --git a/tests/proofmode.v b/tests/proofmode.v
index b235b26ebd17e244dc564fc274380ab636a432a3..5e06d6df43253007fbd4e493130f87a9ff6af086 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1405,6 +1405,11 @@ Lemma test_iFrame_not_add_emp_for_intuitionistically `{!BiAffine PROP} (P : PROP
   □ P -∗ ∃ _ : nat, □ P.
 Proof. iIntros "#H". iFrame "H". Show. by iExists 0. Qed.
 
+Lemma test_auto_iff P : ⊢ P ↔ P.
+Proof. auto. Qed.
+
+Lemma test_auto_wand_iff P : ⊢ P ∗-∗ P.
+Proof. auto. Qed.
 End tests.
 
 Section parsing_tests.