-let rec count_pi = function
- | Cic.Prod (_, _, tgt) -> count_pi tgt + 1
+let strip_pi t = strip_pi [] t
+
+let rec count_pi ctx t =
+ match CicReduction.whd ~delta:true ctx t with
+ | Cic.Prod (n, s, tgt) -> count_pi (Some (n,Cic.Decl s)::ctx) tgt + 1