apply T_14_8
case a.a.h1
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1_left : evalPrime V phi
c1_right : ¬evalPrime V psi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ IsProof (phi.imp_ (psi.not_.imp_ (phi.imp_ psi).not_))
no goals