simp only [map, List.map]
case h.h.h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
head✝ : x✝²
tail✝ : List x✝²
ih : map x✝ tail✝ = List.map x✝ tail✝
⊢ map x✝ (head✝ :: tail✝) = List.map x✝ (head✝ :: tail✝)
case h.h.h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
head✝ : x✝²
tail✝ : List x✝²
ih : map x✝ tail✝ = List.map x✝ tail✝
⊢ x✝ head✝ :: map x✝ tail✝ = x✝ head✝ :: List.map x✝ tail✝