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