Chains over base types

Re-exports the chain instances and lemmas for Option, Sigma, Sum, and constant chains used by the ω-complete partial order infrastructure.