∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {α' : Sort u_1} (g : (a : α) → β a) {f : α' → α} {i : α}
  (a : β i), (∀ (x : α'), f x ≠ i) → (fun j => Function.update g i a (f j)) = fun j => g (f j)