proposition: Lemma subTermsNil (n : nat) (ts : Terms n) (v : nat) (s : Term): ~ In v (freeVarTs ts) -> substTs ts v s = ts.
proof: Proof. intros H; induction ts as [| n t ts Hrects]. - auto. - simpl; unfold freeVarTs in H; rewrite Hrects. + rewrite subTermNil. * reflexivity. * intro H0; elim H; apply in_or_app; auto. + intro H0; elim H; apply in_or_app; auto. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)