intros t z h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (z : { z // Int.abs z < nrows t }), z.val < 0 → nrows (head t z.val) = nrows t - Int.abs z.val
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : { z // Int.abs z < nrows t }
h : z.val < 0
⊢ nrows (head t z.val) = nrows t - Int.abs z.val