Theorem ruleMatchesFEquivalentT : forall s o a r,
  ruleMatchesF s o a r = true <-> ruleMatchesR s o a r.
Proof.
  (* Proof omitted for brevity; see Rules.v for proofs. *)
Qed.
