{motive : IO.FS.Mode → Sort u} →
  (t : IO.FS.Mode) →
    motive IO.FS.Mode.read →
      motive IO.FS.Mode.write →
        motive IO.FS.Mode.writeNew → motive IO.FS.Mode.readWrite → motive IO.FS.Mode.append → motive t