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