Inductive HashValueT :=
  HashValue : forall (s : string),
    matches s (regex "[a-f0-9]{2,256}")
      -> HashValueT.
