Add more lemmas for wand_iff and iff

iris/bi/derived_laws.v

@@ -337,6 +337,11 @@ Global Instance iff_proper :
 
 Lemma iff_refl Q P : Q ⊢ P ↔ P.
 Proof. rewrite /bi_iff; apply and_intro; apply impl_intro_l; auto. Qed.
+Lemma iff_sym P Q : (P ↔ Q) ⊣⊢ (Q ↔ P).
+Proof.
+  apply equiv_entails. split; apply and_intro;
+    try apply and_elim_r; apply and_elim_l.
+Qed.
 
 
 (* BI Stuff *)
@@ -489,6 +494,12 @@ Proof.
   intros HPQ; apply (anti_symm (⊢));
     apply wand_entails; rewrite /bi_emp_valid HPQ /bi_wand_iff; auto.
 Qed.
+Lemma wand_iff_sym P Q :
+  (P ∗-∗ Q) ⊣⊢ (Q ∗-∗ P).
+Proof.
+  apply equiv_entails; split; apply and_intro;
+    try apply and_elim_r; apply and_elim_l.
+Qed.
 
 Lemma entails_impl P Q : (P ⊢ Q) → (⊢ P → Q).
 Proof. intros ->. apply impl_intro_l. auto. Qed.