Theorem keyAssignmentMatchesDecidable : forall k v a,
  {keyAssignmentMatches k v a}+{~keyAssignmentMatches k v a}.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.
