funext _ xs
η : Type u_η
dec_η : DecidableEq η
schema : Schema
⊢ @length = @List.length
case h.h
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝ : Type u_1
xs : List x✝
⊢ length xs = List.length xs