Use constrained concepts across the codebase

This is a follow-up to issue #58

The remaining tasks:

• refactor the codebase to use constrained_message_prop X instead of can_emit (preloaded_with_all_messages_vlsm X)
• possibly also introduce definition in_futures_constrained, which would be in_futures of a preloaded vlsm
• update names of lemmas that were affected by introducing constrained concepts in other places (these were PRs from #358 to #371)
• review the refactorings from the PRs mentioned above and see whether state (preloaded_with_all_messages_vlsm X) should be updated to just state X in any of these