Theorem: LO.Semantics.realize_list_disj (Logic/Logic/Semantics.lean)

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Tarski M
𝓜 : M
l : List F
⊢ 𝓜 ⊧ l.disj ↔ ∃ p ∈ l, 𝓜 ⊧ p
Tactic:
induction l <;> simp [*]
State after:
no goals