∀ {α : Type u_1} {β : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm β} (i : (x : α) → f x ≠ x → β)
  (h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx))
  (hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂) (x : { x // f x ≠ x })
  (motive : (x_1 : { x // f x ≠ x }) → (fun x => ⟨i ↑x ⋯, ⋯⟩) x_1 = (fun x => ⟨i ↑x ⋯, ⋯⟩) x → Prop)
  (x_1 : { x // f x ≠ x }) (h_1 : (fun x => ⟨i ↑x ⋯, ⋯⟩) x_1 = (fun x => ⟨i ↑x ⋯, ⋯⟩) x),
  (∀ (val : α) (property : f val ≠ val) (h : (fun x => ⟨i ↑x ⋯, ⋯⟩) ⟨val, property⟩ = (fun x => ⟨i ↑x ⋯, ⋯⟩) x),
      motive ⟨val, property⟩ h) →
    motive x_1 h_1