+and is_non_recursive ctx paramsno t uri =
+ let t = debrujin_constructor uri 1 [] t in
+(* let ctx, t = split_prods ~subst:[] ctx paramsno t in *)
+ let len = List.length ctx in
+ let rec aux ctx n nn t =
+ match CicReduction.whd ctx t with
+ | Cic.Prod (name,src,tgt) ->
+ does_not_occur ctx n nn src &&
+ aux (Some (name,Cic.Decl src) :: ctx) (n+1) (nn+1) tgt
+ | (Cic.Rel k)
+ | Cic.Appl (Cic.Rel k :: _) when k = nn -> true
+ | t -> assert false
+ in
+ aux ctx (len-1) len t
+