induction xs with
| nil => rfl
| cons _ _ ih =>
  simp only [length, List.length]
  exact congrArg _ ih
case h.h
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝ : Type u_1
xs : List x✝
⊢ length xs = List.length xs
no goals