. intros x y hxy
  cases x
  . cases y
    . rfl
    . contradiction
  . cases y
    . contradiction
    . cases hxy; rfl
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 hxs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
case hxs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))