Description: An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015)