fact: Record Model : Type := model {U : Set; func : forall f : Functions L, naryFunc U (arityF L f); rel : forall r : Relations L, naryRel U (arityR L r)}.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)