*_seq'* -> *_seq_Rbar*

Diff' -> Compl_loc
_iff -> _equiv

For Dynkin pi-lambda too.

Its usage is very similar.

Comment lemmas using not yet proved results.

Change argument gen into generic subset system P when appropriate.
Most results on Psysts are now with the sole witness emptyset.

Lambda -> Lsyst.
Only one Hint DB (= subset_systems).

Extract stuff on subset system generation into Subset_system_gen.

Add Union*_finite_closure, and some facts about them.
Proof of properties of Explicit_ring.
Add properties on is_Semi_algebra.
Rename old lemma Algebra_product_explicit into Algebra_product_explicit_wrong (which should disappear).

sequences (A n).
- Finish the proof of muX2_measurable_finite_aux1, muX2_measurable_finite_aux2,
muX2_measurable_finite_aux3 lemmas.
- Work on the proof of Algebra_product_explicit lemma of subset_system file.

This reverts commit ab8689c9, reversing
changes made to eb9897ee.