dsimp only [relabel]
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ relabel f x = relabel g x
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ List.map (Clause.relabel f) x = List.map (Clause.relabel g) x