∀ {α : Type u} {β : ULift.{u_2, u} α → Type u_1} [inst : DecidableEq α] (f : (a : α) → β { down := a }) (a : α)
  (x : β { down := a }),
  (fun t => ULift.rec (Function.update f a x) t) = Function.update (fun t => ULift.rec f t) { down := a } x