read about inversion. TODO: what is the meaning of [a] = [b] -> a = b, when a and of b (of type X) might not be comparable for equality? e.g. both are functions