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_And xs     => forallb (exprMatchObjectEvalF o) xs
  | EMO_Or xs      => existsb (exprMatchObjectEvalF o) xs
  end.
