further simplified injections_equiv proof