Hint to introduce BI version of `↔ `.
Lemma test_auto_iff P : ⊢ P ↔ P.
Proof. auto. (* fails, fixed by this MR *) Qed.
Lemma test_auto_wand_iff P : ⊢ P ∗-∗ P.
Proof. auto. (* already worked *) Qed.
Edited by Robbert Krebbers
Lemma test_auto_iff P : ⊢ P ↔ P.
Proof. auto. (* fails, fixed by this MR *) Qed.
Lemma test_auto_wand_iff P : ⊢ P ∗-∗ P.
Proof. auto. (* already worked *) Qed.