intros
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (subsch : RetypedSubschema sch) (t : Table sch) (f : Row sch → Row (RetypedSubschema.toSchema subsch)),
    nrows (update subsch t f) = nrows t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
subsch✝ : RetypedSubschema sch
t✝ : Table sch
f✝ : Row sch → Row (RetypedSubschema.toSchema subsch✝)
⊢ nrows (update subsch✝ t✝ f✝) = nrows t✝