rintro ⟨𝓜, h𝓜⟩
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
⊢ Satisfiable M T → (models M T).Nonempty
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
𝓜 : M
h𝓜 : 𝓜 ⊧* T
⊢ (models M T).Nonempty