proposition: Lemma In_freeVarListFormulaE : forall (v : nat) (F : fol.Formulas L), In v (freeVarListFormula F) -> exists f : fol.Formula L, In v (freeVarF f) /\ In f F.
proof: Proof. intros v F H; induction F as [| a F HrecF]. - destruct H. - destruct (in_app_or _ _ _ H) as [H0 | H0]. + exists a; simpl in |- *; auto. + destruct (HrecF H0) as [x Hx]; exists x; cbn; tauto. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)