apply List.length_map
η : Type u_η
dec_η : DecidableEq η
sch : Schema
subsch✝ : RetypedSubschema sch
t✝ : Table sch
f✝ : Row sch → Row (RetypedSubschema.toSchema subsch✝)
⊢ List.length (List.map (fun r => update.updateCells r (f✝ r)) t✝.rows) = List.length t✝.rows
no goals