Inductive exprMatchObjectEvalR (o : object) : exprMatchObject -> Prop :=
  | EMOR_True : exprMatchObjectEvalR o EMO_True
  | EMOR_WithName :
    forall (t : typeName),
      ivName (oType o) = ivName t ->
        exprMatchObjectEvalR o (EMO_WithType t)
  | EMOR_WithAttributesAll :
    forall (required : AttributeNameMaps.t attributeValue),
      (forall (k : attributeName) (v : attributeValue),
        AttributeNameMaps.MapsTo k v required -> AttributeNameMaps.MapsTo k v (oAttributes o)) ->
          exprMatchObjectEvalR o (EMO_WithAttributesAll required)
  | EMOR_WithAttributesAny :
    forall (required : AttributeNameMaps.t attributeValue),
      (exists k : attributeName,
        (exists v : attributeValue,
          AttributeNameMaps.MapsTo k v required /\ AttributeNameMaps.MapsTo k v (oAttributes o))) ->
            exprMatchObjectEvalR o (EMO_WithAttributesAny required)
  | EMOR_And :
    forall (es : list exprMatchObject),
      Forall (exprMatchObjectEvalR o) es ->
        exprMatchObjectEvalR o (EMO_And es)
  | EMOR_Or :
    forall (es : list exprMatchObject),
      Exists (exprMatchObjectEvalR o) es ->
        exprMatchObjectEvalR o (EMO_Or es)
  .
