+
+let split_with_whd (c, t) =
+ let add s v c = Some (s, Cic.Decl v) :: c in
+ let rec aux whd a n c = function
+ | Cic.Prod (s, v, t) -> aux false ((c, v) :: a) (succ n) (add s v c) t
+ | v when whd -> (c, v) :: a, n
+ | v -> aux true a n c (CicReduction.whd c v)
+ in
+ aux false [] 0 c t