intros a
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
⊢ ∀ (a : A), Option.map f (some a) = some (f a)
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
a : A
⊢ Option.map f (some a) = some (f a)