Inductive exprMatchActionEvalR (a : action) : exprMatchAction -> Prop :=
  | EMAR_True : exprMatchActionEvalR a EMA_True
  | EMAR_WithName :
    forall (x : actionName),
      ivName (aName a) = ivName x ->
        exprMatchActionEvalR a (EMA_WithName x)
  | EMAR_And :
    forall (es : list exprMatchAction),
      Forall (exprMatchActionEvalR a) es ->
        exprMatchActionEvalR a (EMA_And es)
  | EMAR_Or :
    forall (es : list exprMatchAction),
      Exists (exprMatchActionEvalR a) es ->
        exprMatchActionEvalR a (EMA_Or es)
  .
