Reduce use of classical axioms

[Lysxia]

Non-exhaustive list of uses:

• Label ordering is defined by a relation leq : L -> L -> Prop, with strict comparison "less than" encoded as ~ leq _ _, which leads to sometimes using excluded middle. Alternative: make label ordering decidable (leb : L -> L -> bool).
• Indistinguishability requires special handling of events E A with empty response types A = False, again requiring excluded middle. Alternative: determine emptiness from the event, adding an assumption E A -> inhabited A \/ ~ inhabited A.
• There are a module or two that use the bisim_is_eq axiom. Alternative: prove the necessary congruence (Proper) lemmas.