a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a → ¬b) ∧ (¬b → a) ↔ (b → ¬a) ∧ (¬a → b)
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a ↔ ¬b) ↔ (b ↔ ¬a)
rw [@iff_def a, @iff_def b]
no goals
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a → ¬b) ∧ (¬b → a) ↔ (b → ¬a) ∧ (¬a → b)
exact and_congr imp_not_comm not_imp_comm