case true_ =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_true_
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑true_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V true_)
no goals