proposition: Lemma In_freeVarListFormula : forall (v : nat) (f : fol.Formula L) (F : fol.Formulas L), In v (freeVarF f) -> In f F -> In v (freeVarListFormula F).
proof: Proof. intros v f F H H0; induction F as [| a F HrecF]. - elim H0. - destruct H0 as [H0| H0]; simpl in |- *. + apply in_or_app; left; now rewrite H0. + apply in_or_app; auto. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)