Changes

Summary

1. clarified heading
2. a quasi-recursive characterization of the multiset order (by Christian Sternagel)
3. merged
4. avoid spurious fact index, notably in "context begin" (via Bundle.context);
5. tuned;
6. tuned;
7. tuned;