induction xs
α : Type
f : α → α
xs : List α
h1 : ∀ x ∈ xs, f x = x
⊢ map f xs = xs
case nil
α : Type
f : α → α
h1 : ∀ x ∈ [], f x = x
⊢ map f [] = []

case cons
α : Type
f : α → α
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x = x) → map f tail✝ = tail✝
h1 : ∀ x ∈ head✝ :: tail✝, f x = x
⊢ map f (head✝ :: tail✝) = head✝ :: tail✝