let equal_sorts ctx t1 t2 = Z3.is_eq_sort ctx t1 t2