fact: Fixpoint substT (s : fol.Term L) (x : nat) (t : fol.Term L) {struct s} : fol.Term L := match s with | var v => match eq_nat_dec x v with | left _ => t | right _ => var v end | apply f ts => apply f (substTs _ ts x t) end with substTs (n : nat) (ss : fol.Terms L n) (x : nat) (t : fol.Term L) {struct ss} : fol.Terms L n := match ss in (fol.Terms _ n0) return (fol.Terms L n0) with | Tnil => Tnil | Tcons m s ts => Tcons (substT s x t) (substTs m ts x t) end.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)