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

State before:
α✝ : Type
x : CNF α✝
β✝ : Type
g : β✝ → Bool
f : α✝ → β✝
h : x.sat (g ∘ f)
⊢ (relabel f x).sat g
Tactic:
simp_all [sat]
State after:
no goals