Lemma clipsNonEmpty : forall (s : clips),
  [] <> clipsList s.
Proof.
  (* Proof omitted for brevity; see Clip.v for proofs. *)
Qed.
