case andE2 ih => exact (ih hv).2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝
no goals