proposition: Lemma subSubTerms (n : nat) (ts : Terms n) (v1 v2 : nat) (s1 s2 : Term): v1 <> v2 -> ~ In v1 (freeVarT s2) -> substTs (substTs ts v1 s1) v2 s2 = substTs (substTs ts v2 s2) v1 (substT s1 v2 s2).
proof: Proof. intros H H0; induction ts as [| n t ts Hrects]. - reflexivity. - simpl in |- *; rewrite Hrects, subSubTerm. + reflexivity. + assumption. + assumption. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(ListExt folProp folProof folLogic subProp folReplace)