Inductive exprMatchSubjectEvalR (s : subject) : exprMatchSubject -> Prop :=
  | EMSR_True :
      exprMatchSubjectEvalR s EMS_True
  | EMSR_WithRolesAll :
    forall (r : RoleSets.t),
      RoleSets.Subset r (sRoles s) ->
        exprMatchSubjectEvalR s (EMS_WithRolesAll r)
  | EMSR_WithRolesAny :
    forall (r : RoleSets.t),
      (exists x, RoleSets.In x r /\ RoleSets.In x (sRoles s)) ->
        exprMatchSubjectEvalR s (EMS_WithRolesAny r)
  | EMSR_And :
    forall (es : list exprMatchSubject),
      Forall (exprMatchSubjectEvalR s) es ->
        exprMatchSubjectEvalR s (EMS_And es)
  | EMSR_Or :
    forall (es : list exprMatchSubject),
      Exists (exprMatchSubjectEvalR s) es ->
        exprMatchSubjectEvalR s (EMS_Or es)
  .
