Fixpoint exprMatchActionEvalF
  (a : action)
  (e : exprMatchAction)
: bool :=
  match e with
  | EMA_False      => false
  | EMA_True       => true
  | EMA_WithName n => eqb (ivName (aName a)) (ivName n)
  | EMA_And xs     => forallb (exprMatchActionEvalF a) xs
  | EMA_Or xs      => existsb (exprMatchActionEvalF a) xs
  end.
