proposition: Lemma freeVarClosedList2 : forall (l : list nat) (v : nat) (x : fol.Formula L), In v (freeVarF (closeList l x)) -> In v (freeVarF x).
proof: Proof. intro l; induction l as [| a l Hrecl]. - simpl; intros v x H; apply H. - simpl; intros v x H; apply Hrecl; eapply in_remove; apply H. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)