proposition: Lemma freeVarSubFormula2 (f : Formula): forall (v : nat) (s : Term) (x : nat), In x (freeVarT s) -> In v (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 |- *; apply in_or_app. induction (in_app_or _ _ _ H0) as [? | ?]. + left; apply freeVarSubTerm2; auto. + right; apply freeVarSubTerm2; auto. - intros r t v s x H H0; rewrite subFormulaRelation; simpl in H0 |- *. apply freeVarSubTerms2; auto. - intros f0 H f1 H0 v s x H1 H2; rewrite subFormulaImp. simpl in H2 |- *; apply in_or_app. induction (in_app_or _ _ _ H2). + left; apply H; auto. + right; apply H0; 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). + simpl in H1; elim (in_remove_neq _ eq_nat_dec _ _ _ H1); auto. + induction (In_dec eq_nat_dec v (freeVarT s)) as [a0 | b0]. * 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. rewrite <- H2; auto. -- apply H. ++ unfold lt_depth; rewrite subFormulaDepth; simpl; apply Nat.lt_succ_diag_r. ++ assumption. ++ apply freeVarSubFormula1. ** assumption. ** simpl in H1; eapply in_remove. apply H1. * simpl; eapply in_in_remove. -- unfold not in |- *; intros. elim b0; now rewrite H2 in H0. -- apply H. apply depthForall; auto. auto. eapply in_remove. simpl in H1; apply H1. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)