split_ifs
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (phi.imp_ psi) then phi.imp_ psi else (phi.imp_ psi).not_)
case pos
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
h✝ : evalPrime V (phi.imp_ psi)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi)

case neg
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
h✝ : ¬evalPrime V (phi.imp_ psi)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi).not_