simp only [groupBySubtractive, groupBy, getColumn2]
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates (getColumn2 (groupBySubtractive t c) "key")
η : 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 r => getValue r "key")
      (List.map
        (fun klv =>
          Row.cons (Cell.fromOption (Option.map ULift.up klv.fst))
            (Row.cons (Cell.val { rows := List.map (fun r => Row.removeColumn (Schema.colImpliesName hc) r) klv.snd })
              Row.nil))
        (List.groupByKey (List.map (fun r => (getValue r c, r)) t.rows))))