proposition: Lemma subFormulaForall2 : forall (f : fol.Formula L) (x v : nat) (s : fol.Term L), exists nv : nat, ~ In nv (freeVarT s) /\ nv <> v /\ ~ In nv (remove eq_nat_dec x (freeVarF f)) /\ substF (forallH x f) v s = match eq_nat_dec x v with | left _ => forallH x f | right _ => forallH nv (substF (substF f x (var nv)) v s) end.
proof: Proof. intros f x v s; rewrite subFormulaForall. induction (eq_nat_dec x v) as [a | b]. - set (A1 := v :: freeVarT s ++ remove eq_nat_dec x (freeVarF f)) in *. exists (newVar A1); repeat split. + unfold not in |- *; intros; elim (newVar1 A1). unfold A1 in |- *; right. apply in_or_app; auto. + unfold not in |- *; intros; elim (newVar1 A1). rewrite H; left; auto. + unfold not in |- *; intros; elim (newVar1 A1). right; apply in_or_app; auto. - induction (In_dec eq_nat_dec x (freeVarT s)) as [a | b0]. + set (A1 := v :: freeVarT s ++ freeVarF f) in *. exists (newVar A1); repeat split. * unfold not in |- *; intros; elim (newVar1 A1); right. apply in_or_app; auto. * unfold not in |- *; intros; elim (newVar1 A1); rewrite H; left; auto. * unfold not in |- *; intros; elim (newVar1 A1); right; apply in_or_app. right; eapply in_remove; apply H. + exists x; repeat split; auto. intro H; eapply (in_remove_neq _ _ _ _ _ H). * reflexivity. * now rewrite subFormulaId. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)