Theorem valueHasTypeDecidable : forall (v : componentValueT) t,
  {valueHasType v t}+{~valueHasType v t}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
