∀ {α : Type u_1} [inst : DecidableEq α]
  (motive :
    (x : ℤ) →
      (x_1 x_2 : α) →
        (x_3 : Equiv.Perm α) → (Equiv.swap x_2 (x_3 x_2) * x_3) x_1 ≠ x_1 → (x_3 ^ x) (x_3 x_2) = x_1 → Prop)
  (x : ℤ) (x_1 x_2 : α) (x_3 : Equiv.Perm α) (x_4 : (Equiv.swap x_2 (x_3 x_2) * x_3) x_1 ≠ x_1)
  (x_5 : (x_3 ^ x) (x_3 x_2) = x_1),
  (∀ (n : ℕ) (x x_6 : α) (x_7 : Equiv.Perm α) (hb : (Equiv.swap x_6 (x_7 x_6) * x_7) x ≠ x)
      (h : (x_7 ^ ↑n) (x_7 x_6) = x), motive (Int.ofNat n) x x_6 x_7 hb h) →
    (∀ (n : ℕ) (b x : α) (f : Equiv.Perm α) (hb : (Equiv.swap x (f x) * f) b ≠ b) (h : (f ^ Int.negSucc n) (f x) = b),
        motive (Int.negSucc n) b x f hb h) →
      motive x x_1 x_2 x_3 x_4 x_5