exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).2
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ f ⋯.choose = f a
no goals