let is_identity (_, context, ugraph) eq =
let _,_,(ty,left,right,_),menv,_ = open_equality eq in
(* doing metaconv here is meaningless *)
- fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+ left = right
+(* fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+ * *)
;;