let is_identity (_, context, ugraph) eq =
let _,_,(ty,left,right,_),menv,_ = open_equality eq in
(* doing metaconv here is meaningless *)
let is_identity (_, context, ugraph) eq =
let _,_,(ty,left,right,_),menv,_ = open_equality eq in
(* doing metaconv here is meaningless *)