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)
ν : Type u_1
neg : Bool
f : PropForm ν
⊢ toPropFun (ofPropForm neg f) = if neg = true then ⟦PropForm.neg f⟧ else ⟦f⟧
no goals