proposition: Lemma freeVarSubTerms3 (n : nat) (ts : fol.Terms L n) (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).
proof: Proof. intros H; induction ts as [| n t ts Hrects]. - left; apply H. - simpl in H; unfold freeVarTs in H; fold (freeVarT (substT t v s)) in H; fold (freeVarTs (substTs ts v s)) in H; induction (in_app_or _ _ _ H) as [H0 | H0]. + induction (freeVarSubTerm3 _ _ _ _ H0) as [H1 | H1]. * left. apply in_in_remove. -- eapply in_remove_neq; apply H1. -- unfold freeVarTs; fold (freeVarT t); fold (freeVarTs ts); apply in_or_app. left; eapply in_remove; apply H1. * now right. + induction (Hrects H0) as [H1 | H1]. * left; apply in_in_remove. -- eapply in_remove_neq; apply H1. -- unfold freeVarTs; fold (freeVarT t); fold (freeVarTs ts); apply in_or_app; right. eapply in_remove; apply H1. * now right. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)