Theorem exprMatchSubjectEvalRolesAnyEmpty : forall s,
  false = exprMatchSubjectEvalF s (EMS_WithRolesAny RoleSets.empty).
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.
