Merge changes to the main repository

1. I have eliminated almost all use of "match" and "fix" from the uu0.v The only matches left are the ones related to the coproducts and to bool. Otherwise the file consistently uses eliminators (induction principles).

2. I continue shortening the lines to approx. 100 characters.

3. New material added in the Current_work directory, including all of the axioms of a C0-system in Csystems.v