Theorem: LeanSAT.Encode.Tseitin.NegNormForm.toPropFun_cleanup (LeanSAT/Encode/Tseitin.lean)

State before:
ν : Type u_1
f : NegNormForm ν
⊢ toPropFun (cleanup f) = toPropFun f
Tactic:
apply Eq.symm
State after:
case h
ν : Type u_1
f : NegNormForm ν
⊢ toPropFun f = toPropFun (cleanup f)

State before:
case h
ν : Type u_1
f : NegNormForm ν
⊢ toPropFun f = toPropFun (cleanup f)
Tactic:
induction f <;>
  aesop (add norm 1 simp ofPropForm)
        (add norm 1 simp toPropFun)
        (add norm 1 simp cleanup)
State after:
no goals