[ ] 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.
Non-exhaustive list of uses:
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).E Awith empty response typesA = False, again requiring excluded middle. Alternative: determine emptiness from the event, adding an assumptionE A -> inhabited A \/ ~ inhabited A.bisim_is_eqaxiom. Alternative: prove the necessary congruence (Proper) lemmas.