proposition: Lemma freeVarSubTerm3 (t : Term): forall (v : nat) (s : Term) (x : nat), In x (freeVarT (substT t v s)) -> In x (List.remove eq_nat_dec v (freeVarT t)) \/ In x (freeVarT s).
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => forall (v : nat) (s : Term) (x : nat), In x (freeVarTs (substTs ts v s)) -> In x (List.remove eq_nat_dec v (freeVarTs ts)) \/ In x (freeVarT s)). - intros n v s x H; simpl in H. induction (eq_nat_dec v n) as [a | b]. + now right. + left; apply in_in_remove. * intro H0; rewrite H0 in H; destruct H as [H| H]. -- congruence. -- contradiction H. * assumption. - intros f t0 H v s x H0; simpl in H0; induction (H _ _ _ H0); auto. - auto. - intros n t0 H t1 H0 v s x H1; simpl in H1; unfold freeVarTs in H1; fold (freeVarT (substT t0 v s)) in H1; fold (freeVarTs (substTs t1 v s)) in H1. destruct (in_app_or _ _ _ H1) as [H2 | H2]. + induction (H _ _ _ H2) as [H3 | H3]. * left; apply in_in_remove. -- eapply in_remove_neq; apply H3. -- unfold freeVarTs; apply in_or_app; left. eapply in_remove; apply H3. * auto. + induction (H0 _ _ _ H2) as [H3 | H3]. * left; apply in_in_remove. -- eapply in_remove_neq; apply H3. -- unfold freeVarTs; fold (freeVarT t0); fold (freeVarTs t1); apply in_or_app. right; eapply in_remove; apply H3. * auto. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)