rw [map, hi]
case cons
α β : Type u
γ : Type w
a : α
as : List α
hi : map id as = as
⊢ map id (a :: as) = a :: as
case cons
α β : Type u
γ : Type w
a : α
as : List α
hi : map id as = as
⊢ id a :: as = a :: as