proposition: Lemma freeVarListFormulaApp : forall a b : fol.Formulas L, freeVarListFormula (a ++ b) = freeVarListFormula a ++ freeVarListFormula b.
proof: Proof. intros a b; induction a as [| a a0 Hreca]. - reflexivity. - simpl in |- *; rewrite Hreca; now rewrite app_assoc. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)