exact congrArg _ ih
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
no goals