have hb : (fun _ : α => b) (choice inferInstance) = b := rfl
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
ha : (fun x => a) (choice (_ : Nonempty α)) = a
⊢ a = b
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
ha : (fun x => a) (choice (_ : Nonempty α)) = a
hb : (fun x => b) (choice (_ : Nonempty α)) = b
⊢ a = b