Description: An equality inference for the maps-to notation. Compare mpteq12dv . (Contributed by Scott Fenton, 8-Aug-2013) (Revised by Mario Carneiro, 11-Dec-2016) (Proof shortened by SN, 11-Nov-2024)