sig
  type pack = { ar : Term.constr; value : Term.constr; morph : Term.constr; }
  val typ : Term.constr lazy_t
  val mk_pack : AAC_coq.Relation.t -> AAC_theory.Sym.pack -> Term.constr
  val null : AAC_coq.Relation.t -> Term.constr
end