let g : β → α := fun b =>
  if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
case inl.intro
α β : 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
⊢ x.unsat
case inl.intro
α β : 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₀
⊢ x.unsat