intros p
A B : Type
f : A → B
inj : Injective f
x y : Option A
⊢ Option.map f x = Option.map f y → x = y
A B : Type
f : A → B
inj : Injective f
x y : Option A
p : Option.map f x = Option.map f y
⊢ x = y