let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
match (build_segments ~terms:[t1; t2]) with
| (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
match (build_segments ~terms:[t1; t2]) with
| (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin