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