exact h₂ h
case intro.inr
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ U
⊢ 𝓜 ⊧ f
no goals