intros x y hxy
case hf
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ Function.injective (Option.map ULift.up)
case hf
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
x y : Option τ
hxy : Option.map ULift.up x = Option.map ULift.up y
⊢ x = y