Lemma componentValuesHaveTypesConsCombine0 : forall xs ys x y,
  componentValuesHaveTypes ((x,y) :: (combine xs ys))
    -> componentValuesHaveTypes (combine xs ys).
Proof.
  (** Proof omitted for brevity. *)
Qed.
