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