Theorem: insightFromGeneralization (NazgandLean4/Prop.lean)

State before:
p₀ p₁ p₂ : Prop
⊢ (p₀ ↔ p₁ → p₂) → p₁ → (p₀ ↔ p₂)
Tactic:
tauto
State after:
no goals