∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (motive : (x x_1 : OpenPartialHomeomorph X Y) → x.toPartialEquiv = x_1.toPartialEquiv → Prop)
  (x x_1 : OpenPartialHomeomorph X Y) (x_2 : x.toPartialEquiv = x_1.toPartialEquiv),
  (∀ (toPartialEquiv : PartialEquiv X Y) (open_source : IsOpen toPartialEquiv.source)
      (open_target : IsOpen toPartialEquiv.target)
      (continuousOn_toFun : ContinuousOn (↑toPartialEquiv) toPartialEquiv.source)
      (continuousOn_invFun : ContinuousOn toPartialEquiv.invFun toPartialEquiv.target)
      (open_source_1 : IsOpen toPartialEquiv.source) (open_target_1 : IsOpen toPartialEquiv.target)
      (continuousOn_toFun_1 : ContinuousOn (↑toPartialEquiv) toPartialEquiv.source)
      (continuousOn_invFun_1 : ContinuousOn toPartialEquiv.invFun toPartialEquiv.target),
      motive
        { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
          continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun }
        { toPartialEquiv := toPartialEquiv, open_source := open_source_1, open_target := open_target_1,
          continuousOn_toFun := continuousOn_toFun_1, continuousOn_invFun := continuousOn_invFun_1 }
        ⋯) →
    motive x x_1 x_2