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

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