{α : Type u_5} →
  {β : Type u_6} →
    {motive : PartialEquiv α β → Sort u} →
      (t : PartialEquiv α β) →
        ((toFun : α → β) →
            (invFun : β → α) →
              (source : Set α) →
                (target : Set β) →
                  (map_source' : ∀ ⦃x : α⦄, x ∈ source → toFun x ∈ target) →
                    (map_target' : ∀ ⦃x : β⦄, x ∈ target → invFun x ∈ source) →
                      (left_inv' : ∀ ⦃x : α⦄, x ∈ source → invFun (toFun x) = x) →
                        (right_inv' : ∀ ⦃x : β⦄, x ∈ target → toFun (invFun x) = x) →
                          motive
                            { toFun := toFun, invFun := invFun, source := source, target := target,
                              map_source' := map_source', map_target' := map_target', left_inv' := left_inv',
                              right_inv' := right_inv' }) →
          motive t