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