Explain the transformation rewrite attempts step by step

[sgraf812]

What question should the reference manual answer?

How does the rewrite tactic proceed? Which steps would I perform if I were to do it manually?

Additional context

The improved error message "error: tactic 'rewrite' failed, motive is not type correct" is really helpful and contains the explanation I was looking for (reformatted for better presentation):

First, it looks for all 'a' in 'e'.
Second, it tries to abstract these occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, with the property that 'm a' is definitionally equal to 'e'.
Third, we observe that 'congrArg' implies that 'm a = m b', which can be used with lemmas such as 'Eq.mpr' to change the goal.
However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.

Possible solutions: 
* Use rewrite's 'occs' configuration option to limit which occurrences are rewritten.
* Use 'simp' or 'conv' mode, which have strategies for certain kinds of dependencies (these tactics can handle proofs and 'Decidable' instances whose types depend on the rewritten term, and 'simp' can apply user-defined '@[congr]' theorems as well).

Perhaps some of this wisdom could be added to the reference manual entry for rewrite. This improved entry could include the example from test case motiveNotTypeCorrect and perhaps exemplify the workarounds.