- (almost) proved read with help of a few assumptions.
- Some fixes on definitions. Also a few proofs, mainly set2facts/U-inversion.