Fixpoint exprMatchObjectEvalF
  (o : object)
  (e : exprMatchObject)
: bool :=
  match e with
  | EMO_False => false
  | EMO_True => true
  | EMO_WithType n =>
    eqb (ivName (oType o)) (ivName n)
  | EMO_WithAttributesAll attributesRequired =>
    let attributesHeld := oAttributes o in
      forallb (fun p => mapsB attributesHeld (fst p) (snd p))
        (AttributeNameMaps.elements attributesRequired)
  | EMO_WithAttributesAny attributesRequired =>
    let attributesHeld := oAttributes o in
      existsb (fun p => mapsB attributesHeld (fst p) (snd p))
        (AttributeNameMaps.elements attributesRequired)
  | EMO_And xs =>
    forallb (exprMatchObjectEvalF o) xs
  | EMO_Or xs =>
    existsb (exprMatchObjectEvalF o) xs
  end.
