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

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
⊢ ¬Meaningful 𝓜 ↔ ∀ (f : F), 𝓜 ⊧ f
Tactic:
simp [meaningful_iff]
State after:
no goals