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