simp only [length, List.length]
case h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝ : Type u_1
head✝ : x✝
tail✝ : List x✝
ih : length tail✝ = List.length tail✝
⊢ length (head✝ :: tail✝) = List.length (head✝ :: tail✝)
case h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝ : Type u_1
head✝ : x✝
tail✝ : List x✝
ih : length tail✝ = List.length tail✝
⊢ length tail✝ + 1 = List.length tail✝ + 1