Rewrite in lambda expr

Stream: new members

[Björn Fischer]

Can I rewrite subterms of lambda expression (which depend on the argument)? rw does not find the pattern. Illustrative example:

variables (α : Type) (f : (α → α) → Prop)
lemma l (a : α) : id a = a := by refl

example : f (λ a, id a) := begin
    rw l, -- can't find pattern id ?m_2
end

[Mario Carneiro]

use dsimp or simp

[Mario Carneiro]

or conv