Theorem evaluateRulesDefaultDenyNoMatches : forall rs s o a,
  Forall (fun r => ruleMatchesF s o a r = false) rs ->
    evaluateRules rs s o a = AccessDenied.
Proof.
  (* Proof omitted for brevity; see Policies.v for proofs. *)
Qed.
