simp only [nrows, Schema.length_eq_List_length]
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t1 t2 : Table sch
⊢ nrows (vcat t1 t2) = nrows t1 + nrows t2
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t1 t2 : Table sch
⊢ List.length (vcat t1 t2).rows = List.length t1.rows + List.length t2.rows