apply IsDeduct.axiom_
case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (psi.imp_ (phi.imp_ psi))

case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
case a.a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsAxiom (psi.imp_ (phi.imp_ psi))

case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi