Theorem clipEqDec : forall (x y : clip),
  {x = y}+{x <> y}.
Proof.
  (* Proof omitted for brevity; see Clip.v for proofs. *)
Qed.
