cases h1
α : Type
f : α → α
hd : α
tl : List α
ih : (∀ x ∈ tl, f x = x) → map f tl = tl
h1 : f hd = hd ∧ ∀ a ∈ tl, f a = a
⊢ map f (hd :: tl) = hd :: tl
case intro
α : Type
f : α → α
hd : α
tl : List α
ih : (∀ x ∈ tl, f x = x) → map f tl = tl
left✝ : f hd = hd
right✝ : ∀ a ∈ tl, f a = a
⊢ map f (hd :: tl) = hd :: tl