cases z with | mk z prop =>
simp only at h
simp only [nrows, Schema.length_eq_List_length] at prop
simp only [head, nrows, List.dropLastN, Function.comp, h,
           Schema.length_eq_List_length, ite_true]
rw [List.length_reverse, List.length_drop, List.length_reverse]
rw [List.length_reverse]
exact prop
η : 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
no goals