+let rec strip_pi = function
+ | Cic.Prod (_, _, tgt) -> strip_pi tgt
+ | t -> t
+
+let rec count_pi = function
+ | Cic.Prod (_, _, tgt) -> count_pi tgt + 1
+ | t -> 0
+
+let rec type_of_p sort dependent leftno indty = function
+ | Cic.Prod (n, src, tgt) when leftno = 0 ->
+ Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt)
+ | Cic.Prod (_, _, tgt) -> type_of_p sort dependent (leftno - 1) indty tgt
+ | t ->
+ if dependent then
+ Cic.Prod (Cic.Anonymous, indty, Cic.Sort sort)
+ else
+ Cic.Sort sort
+
+let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
+ | Cic.Prod (_, src, tgt) when strip = 0 ->
+ Cic.Prod (fresh_binder true,
+ CicSubstitution.lift_from (liftfrom + 1) liftno src,
+ add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt)
+ | Cic.Prod (_, _, tgt) ->
+ add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt
+ | t ->
+ if dependent then
+ Cic.Prod (fresh_binder dependent,
+ CicSubstitution.lift_from (rightno + 1) liftno indty,
+ Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 0 (rightno + 1)))
+ else
+ Cic.Prod (Cic.Anonymous,
+ CicSubstitution.lift_from (rightno + 1) liftno indty,
+ if rightno = 0 then
+ Cic.Rel (1 + liftno + rightno)
+ else
+ Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 1 rightno))
+
+exception Failure of string
+
+let string_of_sort = function
+ | Cic.Prop -> "Prop"
+ | Cic.CProp -> "CProp"
+ | Cic.Set -> "Set"
+ | Cic.Type _ -> "Type"
+
+let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =