Explicit policy in [respects_policy_at_preemption_point]
As Björn noted, from a readability PoV, it's quite unfortunate that the policy that is being respected doesn't show up in the code. The subject of definitions should show up as an explicit argument, even if it is implicit everywhere else.
Currently we have:
Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
However, ideally, we need:
Hypothesis H_respects_policy : respects_policy_at_preemption_point FP arr_seq sched.
^^ --- new, explicit, argument here