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

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
f : F
⊢ ∅ ⊧ f
Tactic:
rintro h
State after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
f : F
h : M
⊢ h ∈ ∅ → h ⊧ f

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
f : F
h : M
⊢ h ∈ ∅ → h ⊧ f
Tactic:
simp
State after:
no goals