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