intro t rs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (rs : List (Row sch)), nrows (addRows t rs) = nrows t + List.length rs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
rs : List (Row sch)
⊢ nrows (addRows t rs) = nrows t + List.length rs