sig
  val typ : Coq.lazy_ref
  val pair : Coq.lazy_ref
  val of_pair :
    EConstr.constr ->
    EConstr.constr -> EConstr.constr * EConstr.constr -> EConstr.constr
end