Theorem exprMatchActionEvalEquivalentF : forall a e,
  false = exprMatchActionEvalF a e <-> ~exprMatchActionEvalR a e.
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.
