proposition: Lemma freeVarClosedList1 : forall (l : list nat) (v : nat) (x : fol.Formula L), In v l -> ~ In v (freeVarF (closeList l x)).
proof: Proof. intro l; induction l as [| a l Hrecl]. - intros v x H; elim H. - intros v x H; induction H as [H| H]. + simpl in |- *; rewrite H. unfold not in |- *; intros H0; elim (in_remove_neq _ _ _ _ _ H0); reflexivity. + simpl in |- *. intro H0. assert (H1: In v (freeVarF (closeList l x))). { eapply in_remove. apply H0. } apply (Hrecl _ _ H H1). Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)