Theorem exprMatchActionEvalEquivalentT : forall s e,
  true = exprMatchActionEvalF s e <-> exprMatchActionEvalR s e.
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.
