Theorem evaluateRulesLastMatchingPreNoHalt :
  forall (s      : subject)
         (o      : object)
         (a      : action)
         (r      : rule)
         (r_pre  : list rule)
         (r_post : list rule),
  ruleMatchesF s o a r = true ->
    Forall (fun q => ruleDoesNotHaltOnMatch q) r_pre ->
      Forall (fun q => ruleDoesNotMatch s o a q) r_post ->
        evaluateRules (r_pre ++ [r] ++ r_post) s o a = evaluateRules [r] s o a.
Proof.
  (* Proof omitted for brevity; see Policies.v for proofs. *)
Qed.
