Changes

Summary

1. more frugal simp rules for bit operations; more pervasive use of bit selector
2. more scalable output of YXML files;
3. proper grounding of free types produced by reconstruct_proof/infer_type, e.g. relevant for Lattices_Big.semilattice_set.infinite;
4. tuned;
5. tuned whitespace;
6. more thorough strip_shyps for proof boxes (but types are usually stripped and reconstructed later);
7. clarified;
8. tuned signature;
9. tuned signature;
10. tuned signature;