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