fact: Fixpoint interpTermsVector (value : nat -> U M) (n : nat) (ts : Terms L n) {struct ts} : Vector.t (U M) n := match ts in (Terms _ n) return (Vector.t (U M) n) with | Tnil => Vector.nil (U M) | Tcons m t ts => Vector.cons (U M) (interpTerm value t) m (interpTermsVector value m ts) end.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)