+
+(* split_with_whd (c, t) takes a type t typed in the context c and returns
+ [(c_0, t_0); (c_1, t_1); ...; (c_n, t_n)], n where t_0 is the conclusion of
+ t and t_i is the premise of t accessed by Rel i in t_0.
+ Performes a whd on the conclusion before giving up.
+ Each t_i is returned with a context c_i in wich it is typed
+ split_with_normalize (c, t) normalizes t before operating the split
+ whd is useless here
+*)
+val split_with_whd: Cic.context * Cic.term ->
+ (Cic.context * Cic.term) list * int
+val split_with_normalize: Cic.context * Cic.term ->
+ (Cic.context * Cic.term) list * int