let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
let _, context, ugraph = env in
let metasenv = tmetas in
let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
let _, context, ugraph = env in
let metasenv = tmetas in