theorem LawfulFunctor.map_inj_right_of_nonempty {f : Type u_1 → Type u_2} {α β : Type u_1} [Functor f] [LawfulFunctor f] [Nonempty α] {g : α → β} (h : ∀ {x y : α}, g x = g y → x = y) {x y : f α} : g <$> x = g <$> y ↔ x = y

theorem LawfulMonad.map_inj_right {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] {f : α → β} (h : ∀ {x y : α}, f x = f y → x = y) {x y : m α} : f <$> x = f <$> y ↔ x = y