Document relation between Discrete and Timeless (in appendix?)
See discussion in !607 (comment 61127) by @robbertkrebbers:
I also wondered about this a long time ago and came to the same conclusion as you: Discrete P → Timeless P holds, but is not so useful; Timeless P → Discrete P does not hold; discrete propositions are unlikely to exist. It might be worth documenting this somewhere, but I don't know what's the best place. Maybe the appendix?