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 not_imp_comm imp_not_comm