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

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