∀ {overwrite ignoreIfExists overwrite_1 ignoreIfExists_1 : Bool},
  { overwrite := overwrite, ignoreIfExists := ignoreIfExists } =
      { overwrite := overwrite_1, ignoreIfExists := ignoreIfExists_1 } →
    overwrite = overwrite_1 ∧ ignoreIfExists = ignoreIfExists_1