no goals
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), PointedMap.f F (f x) = f' (PointedMap.f F x)
n : ℕ
L : ListBlank Γ
⊢ map F (modifyNth f n L) = modifyNth f' n (map F L)
induction' n with n IH generalizing L <;>
  simp only [*, ListBlank.head_map, ListBlank.modifyNth, ListBlank.map_cons, ListBlank.tail_map]