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