Theorem: LO.Semantics.realize_list_conj (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.conj ↔ ∀ p ∈ l, 𝓜 ⊧ p
Tactic:
induction l <;> simp [*]
State after:
no goals