induction x <;> induction y <;> try trivial
A B : Type
f : A → B
inj : Injective f
x y : Option A
p : Option.map f x = Option.map f y
⊢ x = y
case some.some
A B : Type
f : A → B
inj : Injective f
val✝¹ val✝ : A
p : Option.map f (some val✝¹) = Option.map f (some val✝)
⊢ some val✝¹ = some val✝