+let is_weak_identity (metasenv, context, ugraph) = function
+ | (_, _, (ty, left, right, _), menv, _) ->
+ (left = right ||
+ (meta_convertibility left right))
+ (* the test below is not a good idea since it stops
+ demodulation too early *)
+ (* (fst (CicReduction.are_convertible
+ ~metasenv:(metasenv @ menv) context left right ugraph)))*)
+;;