. cases y
  . rfl
  . contradiction
case hf.none
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
y : Option τ
hxy : Option.map ULift.up none = Option.map ULift.up y
⊢ none = y

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