fact: Fixpoint nnHelp (f : Formula L) : Formula L := match f with | equal t s => equal t s | atomic r ts => atomic r ts | impH A B => impH (nnHelp A) (nnHelp B) | notH A => notH (nnHelp A) | forallH v A => (allH v, ~ ~ nnHelp A)%fol end.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)