(** A proposition that states that two file names are the same if their
    uppercase transformations are the same. *)
Definition fileNamesSame (s t : FileNameT) :=
  match s, t with
  | FileName fs _, FileName ft _ => uppercaseSame fs ft
  end.
