proposition: Lemma subTermsExch (n : nat) (ts : Terms n) (v1 v2 : nat) (s1 s2 : Term): v1 <> v2 -> ~ In v2 (freeVarT s1) -> ~ In v1 (freeVarT s2) -> substTs (substTs ts v1 s1) v2 s2 = substTs (substTs ts v2 s2) v1 s1.
proof: Proof. intros H H0 H1; induction ts as [| n t ts Hrects]. - auto. - simpl; rewrite Hrects, subTermExch; auto. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)