intro (Iff.intro (_ : p₁ → p₂) (_ : p₂ → p₁))
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
⊢ (p₁ ↔ p₂) → (f p₁ ↔ f p₂)
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
⊢ f p₁ ↔ f p₂