Rewrite patterns

We support SSReflect version of rewrite. The general syntax for it is:

srw ([-] [? <|> !] [ [[-] pos*] ] trm)* [at loc]

where

1. [-] is responsible for the rewrite direction: empty for direct and - for reversed
2. [? <|> !] is responsible for the number of times we rewrite: ? for 0 and more and ! for 1 and more
3. [ [[-] [pos*] ] ] is responsible for positions of terms matching thm at which we rewrite: [n_1 n_2 n_3 ...] for rewriting at all n_i positions, [- n_1 n_2 n_3 ...] for rewriting at all positions except n_i and empty for rewriting at all positions
4. thm for the equality which we want to rewrite
5. [at loc] for the location at which we rewrite (empty for rewriting in the goal)

You can also use //, /=, //=, /== and //== inside srw.

example :

srw -![1 3](cat_take_drop i m) //= -?[- 5 6](cat_take_drop i s2) def_m_i -cat_cons at h |-