+
+let is_equational_fact ty =
+ let rec aux ctx t =
+ match CicReduction.whd ctx t with
+ | Cic.Prod (name,src,tgt) ->
+ let s,u =
+ CicTypeChecker.type_of_aux' [] ctx src CicUniv.oblivion_ugraph
+ in
+ if fst (CicReduction.are_convertible ctx s (Cic.Sort Cic.Prop) u) then
+ false
+ else
+ aux (Some (name,Cic.Decl src)::ctx) tgt
+ | Cic.Appl [ Cic.MutInd (u,_,_) ; _; _; _] -> LibraryObjects.is_eq_URI u
+ | _ -> false
+ in
+ aux [] ty
+;;