Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 16-Dec-2013) Drop ax-10 while shortening its proof. (Revised by Steven Nguyen and Gino Giotto, 1-Dec-2023)