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