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