refine (ih₁ hv).elim (fun hA => ih₂ ?_) (fun hB => ih₃ ?_) <;> simp [*]
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
ih₁ : Γ✝ ⊨ A✝ || B✝
ih₂ : insert A✝ Γ✝ ⊨ C✝
ih₃ : insert B✝ Γ✝ ⊨ C✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v C✝
no goals