proposition: Lemma subTermsId : forall (n : nat) (ts : fol.Terms L n) (v : nat), substTs n ts v (var v) = ts.
proof: Proof. intros n ts v; induction ts as [| n t ts Hrects]. - reflexivity. - simpl in |- *; now rewrite Hrects, subTermId. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)