Lemma fileWFIndexDataPresentIffDecidable : forall f,
  {fileWFIndexDataPresentIff f}+{~fileWFIndexDataPresentIff f}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
