apply propCompleteAuxAux P U Δ_U
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' ↑Δ_U) P
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ U' ∈ ↑Δ_U, U'.IsPrime

case h1_U
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U.IsPrime

case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U ∉ ↑Δ_U

case h3
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' ↑Δ_U ∪ {evalPrimeFfToNot V U}) P