Theorem typeNameDec : forall (a b : typeName),
  {a = b}+{a <> b}.
Proof.
  (* Proof omitted for brevity; see Objects.v for proofs. *)
Qed.
