Theorem: CNF.eval_relabel (LeanSAT/Reflect/CNF/Relabel.lean)

State before:
α β : Type
f : α → β
g : β → Bool
x : CNF α
⊢ eval g (relabel f x) = eval (g ∘ f) x
Tactic:
induction x <;> simp_all [relabel]
State after:
no goals