simp
α : Type
f : α → α
hd : α
tl : List α
ih : (∀ x ∈ tl, f x = x) → map f tl = tl
h1_left : f hd = hd
h1_right : ∀ a ∈ tl, f a = a
⊢ map f (hd :: tl) = hd :: tl
α : Type
f : α → α
hd : α
tl : List α
ih : (∀ x ∈ tl, f x = x) → map f tl = tl
h1_left : f hd = hd
h1_right : ∀ a ∈ tl, f a = a
⊢ f hd = hd ∧ map f tl = tl