+and is_non_recursive_singleton (Ref.Ref (uri,_)) iname ity cty =
+ let ctx = [iname, C.Decl ity] in
+ let cty = debruijn uri 1 [] cty in
+ let len = List.length ctx in
+ let rec aux ctx n nn t =
+ match R.whd ctx t with
+ | C.Prod (name, src, tgt) ->
+ does_not_occur ~subst:[] ctx n nn src &&
+ aux ((name, C.Decl src) :: ctx) (n+1) (nn+1) tgt
+ | C.Rel k | C.Appl (C.Rel k :: _) when k = nn -> true
+ | _ -> assert false
+ in
+ aux ctx (len-1) len cty
+