"Reverse" -> "reverse" also in CCS example

Latest updates of the CCS example

* Latest updates of CCS example

* Removed trailing spaces ...

[CCS] MultivariateTheory: general forms of the "unique solution of equations/contractions" theorems

Remove TABs from examples

Document strange uninterruptibility of {PROVE,METIS}_TAC in comment

This may be a regression

Remove proof/use of lemma already present in arithmeticTheory

Make some minor tactic simplifications

These were found in the course of trying to find instances of
uninterruptible PROVE_TACs.

Updated CCS example with some fixed definitions and other small changes

[CCS] Added some further developments on `rooted contraction` (OBS_congr)

- COARSEST_PRECONGR_FINITE: the "coarsest (pre)congruence contained in `contraction` for finite-state CCS
- UNIQUE_SOLUTION_OF_ROOTED_CONTRACTION: a stronger version of UNIQUE_SOLUTION_OF_OBS_CONTRACTION

[CCS] fixed 3 broken lemmas due to changes of irule in d2d6d792.

[CCS] late developments with new theorems; fixed with K11 release; selftest added

[CCS] fixed building CCS example with --stdknl

[CCS] further extensions of the CCS example (thesis project)