have : f p₁ → f p₂ := f_subst ‹p₂ → 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₁
⊢ 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₂