no goals
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : List Γ
⊢ List.headI (List.map f.f l) = Turing.PointedMap.f f (List.headI l)
cases l <;> [exact (PointedMap.map_pt f).symm; rfl]