Definition manifesItemsFilenamesUnique :=
  forall (m : ManifestT),
    forall (i0 : ItemT),
      In i0 (manifestItems m)
        -> ~(exists i1 : ItemT,
               (In i1 (manifestItems m))
            /\ (i0 <> i1)
            /\ (fileNamesSame (itemFileName i0) (itemFileName i1))).
