+let get_uri_of_head = function
+ | C.AConst (_, u, _) ->
+ Some (u, 0, 0, 0)
+ | C.AAppl (_, C.AConst (_, u, _) :: vs) ->
+ Some (u, 0, 0, List.length vs)
+ | C.AMutInd (_, u, i, _) ->
+ Some (u, succ i, 0, 0)
+ | C.AAppl (_, C.AMutInd (_, u, i, _) :: vs) ->
+ Some (u, succ i, 0, List.length vs)
+ | C.AMutConstruct (_, u, i, j, _) ->
+ Some (u, succ i, j, 0)
+ | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: vs) ->
+ Some (u, succ i, j, List.length vs)
+ | _ ->
+ None
+
+let get_uri_of_apply = function
+ | T.Exact (t, _)
+ | T.Apply (t, _) -> get_uri_of_head t
+ | _ -> None
+
+let is_reflexivity st step =
+ match get_uri_of_apply step with
+ | None -> false
+ | Some (uri, i, j, n) ->
+ st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1 && n = 0
+
+let is_ho_reflexivity st step =
+ match get_uri_of_apply step with
+ | None -> false
+ | Some (uri, i, j, n) ->
+ st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1 && n > 0
+
+let are_convertible st pred sx dx =
+ let pred, sx, dx = H.cic pred, H.cic sx, H.cic dx in
+ let sx, dx = C.Appl [pred; sx], C.Appl [pred; dx] in
+ fst (R.are_convertible st.context sx dx Un.default_ugraph)
+