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