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