proposition: Lemma subTermApply : forall (f : Functions L) (ts : fol.Terms L (arityF L f)) (v : nat) (s : fol.Term L), substT (apply f ts) v s = apply f (substTs _ ts v s).
proof: Proof. reflexivity. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)