Inductive ModuleT := Module {
  mFile : FileNameT;
  mHash : HashT;
  mSize : nat
}.
