## Stream: general

### Topic: rewriting

#### Pablo Le Hénaff (Jun 08 2018 at 14:03):

Hey again,
I'm stuck with this rewriting issue, I don't understand why it won't match :'(

#### Pablo Le Hénaff (Jun 08 2018 at 14:04):

set_option pp.all true
example {V : Type} (s : finset V) [decidable_eq V] (x y : V) (h : x ≠ y) :
finset.filter (λ a : V, a = x ∧ a = y) s = finset.filter (λa, false) s :=
begin
have : ∀a : V, a = x ∧ a = y ↔ false := sorry,
rw [this]
end


#### Simon Hudon (Jun 08 2018 at 14:09):

use simp instead. rw does not rewrite bound variables. You need congruence lemmas for that and simp can access them.

#### Chris Hughes (Jun 08 2018 at 20:35):

How come simp can handle rewriting the type of the decidable_pred instance?

#### Simon Hudon (Jun 08 2018 at 20:38):

rewriting decidable is tricky because of how dependent those types are