for a, b being object st a,b are_convertible_wrt {} holds
a = b by Th13;