intro h 𝓜 hf hT
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f) → ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
𝓜 : M
hf : ¬𝓜 ⊧ f
hT : 𝓜 ⊧* T
⊢ False