Theorem: or_iff (SetTheory/Formula.lean)

State before:
V : Type ?u.6497
inst✝ : SetTheory V
p q : Prop
⊢ p ∨ q ↔ ¬p → q
Tactic:
by_cases p <;> aesop
State after:
no goals