split_ifs
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
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_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi.not_.not_ else phi.not_)
case pos
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
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_)
h✝ : evalPrime V phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_.not_

case neg
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
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_)
h✝ : ¬evalPrime V phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_