simp only [nrows, Schema.length_eq_List_length] at prop
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : z < 0
⊢ nrows (head t { val := z, property := prop }.val) = nrows t - Int.abs { val := z, property := prop }.val
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < nrows t
h : z < 0
prop : Int.abs z < List.length t.rows
⊢ nrows (head t { val := z, property := prop✝ }.val) = nrows t - Int.abs { val := z, property := prop✝ }.val