exact Iff.intro ‹f p₁ → f 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₁
this✝ : f p₁ → f p₂
this : f p₂ → f p₁
⊢ f p₁ ↔ f p₂
no goals