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

State before:
ν : Type u_1
neg : Bool
f : PropForm ν
⊢ toPropFun (ofPropForm neg f) = if neg = true then ⟦PropForm.neg f⟧ else ⟦f⟧
Tactic:
induction f generalizing neg <;>
  aesop (add norm 1 simp ofPropForm)
        (add norm 1 simp toPropFun)
        (add norm 1 simp himp_eq)
        (add norm 1 simp PropFun.biImpl_eq_impls)
State after:
no goals