proposition: Lemma subTermsTrans (n : nat) (ts : Terms n) (v1 v2 : nat) (s : Term): ~ In v2 (List.remove eq_nat_dec v1 (freeVarTs ts)) -> substTs (substTs ts v1 (var v2)) v2 s = substTs ts v1 s.
proof: Proof. intros H; induction ts as [| n t ts Hrects]. - auto. - simpl; unfold freeVarTs in H; rewrite Hrects. + rewrite subTermTrans. * reflexivity. * intro H0; elim H; apply in_in_remove. -- eapply in_remove_neq, H0. -- apply in_or_app; left; eapply in_remove, H0. + intro H0; elim H; apply in_in_remove. * eapply in_remove_neq, H0. * apply in_or_app; right; eapply in_remove, H0. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)