proposition: Lemma freeVarSubFormula4 (f : Formula) : forall (v : nat) (s : Term) (x : nat), In x (freeVarF (substF f v s)) -> ~ In v (freeVarF f) -> In x (freeVarF f).
proof: Proof. elim f using Formula_depth_ind2. - intros t t0 v s x H H0; rewrite subFormulaEqual in H. simpl in H, H0 |- *; apply in_or_app. induction (in_app_or _ _ _ H) as [H1 | H1]. + left; eapply freeVarSubTerm4. * apply H1. * intro H2; elim H0. apply in_or_app; now left. + right; eapply freeVarSubTerm4. * apply H1; intro H2; elim H0; apply in_or_app; now right. * intro H2; apply H0; apply in_or_app; now right. - intros r t v s x H H0; rewrite subFormulaRelation in H. simpl in H |- *; eapply freeVarSubTerms4; [apply H | assumption]. - intros f0 H f1 H0 v s x H1 H2; rewrite subFormulaImp in H1; simpl in H2, H1 |- *; apply in_or_app. induction (in_app_or _ _ _ H1) as [H3 | H3]. + left; eapply H. * apply H3. * intro H4; elim H2; apply in_or_app; now left. + right; eapply H0. * apply H3. * intro H4; elim H2; apply in_or_app; now right. - intros f0 H v s x H0 H1; rewrite subFormulaNot in H0. simpl; eapply H. + apply H0. + apply H1. - intros v a H v0 s x H0 H1; simpl in |- *. simpl in H1; rewrite subFormulaForall in H0. induction (eq_nat_dec v v0) as [a0 | ?]. + apply H0. + induction (In_dec eq_nat_dec v (freeVarT s)) as [a0 | ?]. * set (nv := newVar (v0 :: freeVarT s ++ freeVarF a)). simpl in H0. assert (H2: In x (freeVarF (substF (substF a v (var nv)) v0 s))). { eapply in_remove; apply H0. } assert (H3: In x (freeVarF (substF a v (var nv)))). { eapply H. - unfold lt_depth; rewrite subFormulaDepth. apply depthForall. - apply H2. - intros H3; induction (freeVarSubFormula3 _ _ _ _ H3). + auto. + elim (newVar1 (v0 :: freeVarT s ++ freeVarF a)). fold nv; induction H4 as [H4| H4]. * rewrite H4; simpl; now left. * elim H4. } induction (freeVarSubFormula3 _ _ _ _ H3). -- assumption. -- induction H4 as [H4| H4]. ++ elim (in_remove_neq _ _ _ _ _ H0); now subst nv. ++ elim H4. * simpl in H0; apply in_in_remove. -- eapply in_remove_neq, H0. -- eapply H. ++ apply depthForall. ++ eapply in_remove, H0. ++ intro H2; elim H1. ** apply in_in_remove; auto. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)