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

State before:
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
x : CNF α✝
⊢ relabel f (relabel g x) = relabel (f ∘ g) x
Tactic:
simp only [relabel, List.map_map, Clause.relabel_relabel']
State after:
no goals