simp only [relabel]
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ relabel f x = relabel g x
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ List.map (fun x => (f x.fst, x.snd)) x = List.map (fun x => (g x.fst, x.snd)) x