proposition: Lemma freeVarNNHelp (f : Formula L): freeVarF f = freeVarF (nnHelp f).
proof: Proof. induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; try reflexivity. - simpl; now rewrite Hrecf1, Hrecf0. - simpl; assumption. - simpl; now rewrite Hrecf. Qed.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)