Lemma length_eq_dec : forall {A B : Type} (xs : list A) (ys : list B),
  {length xs = length ys}+{~(length xs = length ys)}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
