intros
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
⊢ ∀ (t : Table sch) (f : Row sch → Fin (nrows t) → Row sch'), nrows (select t f) = nrows t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
t✝ : Table sch
f✝ : Row sch → Fin (nrows t✝) → Row sch'
⊢ nrows (select t✝ f✝) = nrows t✝