Theorem componentValuesHaveTypesDecidable : forall ps,
  {componentValuesHaveTypes ps}+{~componentValuesHaveTypes ps}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
