rw [List.map_congr]
α β : 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
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ ∀ (x_1 : α × Bool), x_1 ∈ x → (f x_1.fst, x_1.snd) = (g x_1.fst, x_1.snd)