exact Schema.length_eq_List_length ▸ prop
case mk.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < Schema.length t.rows
prop : Int.toNat z < Schema.length t.rows
h : { val := z, property := prop✝ }.val ≥ 0
h_not_neg : ¬z < 0
⊢ Int.toNat z < List.length t.rows
no goals