+ (** can't build the required elimination principle (e.g. elimination from Prop
+ * to Set *)
+exception Can_t_eliminate
+
+ (** internal error while generating elimination principle *)
+exception Elim_failure of string
+
+(** @param sort target sort, defaults to Type
+* @param uri inductive type uri