conv =>
  rhs
  lhs
  apply funext (g := _) _
  apply (λ x => Option.map ULift.up ∘ Prod.fst)
  apply (λ x => rfl)
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (fun x => Option.map ULift.up x.fst)
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map ((fun x => Option.map ULift.up ∘ Prod.fst) (Row sch))
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))