∀ {α : Type u_1} {β : Type u_2} {p : β → Prop} [inst : DecidablePred p] {f : α ≃ Subtype p} {g₁ g₂ : Equiv.Perm α}
  {t : Set α},
  Set.RightInvOn (⇑g₁) (⇑g₂) t → Set.RightInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' t)