rcases nonempty_or_impossible x with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩)
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
⊢ (relabel f x).unsat ↔ 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₀ : α
⊢ (relabel f x).unsat ↔ x.unsat

case inr.intro
α β : Type
f : α → β
n : Nat
w : ∀ {a b : α}, mem a (List.replicate n []) → mem b (List.replicate n []) → f a = f b → a = b
⊢ (relabel f (List.replicate n [])).unsat ↔ unsat (List.replicate n [])