If you have an equation of the form eqn : (x : t) → foo x ≡ bar x, is it possible to use rewrite in such a way that it picks up all instances of foo x and rewrites them, or do you always have to manually apply eqn to the right terms before you can give it to rewrite?<br>