for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
[:U1,U2:],U1 are_similar