∀ {α : Type u_1} [inst : DecidableEq α] {β : Type u_2} (a : α) (σ : Equiv.Perm β)
  (motive :
    (x : α × β) →
      (Equiv.Perm.prodExtendRight a σ) x ≠ x →
        (Equiv.Perm.prodExtendRight a σ) ((Equiv.Perm.prodExtendRight a σ) x) ≠ (Equiv.Perm.prodExtendRight a σ) x →
          Prop)
  (x : α × β) (hab : (Equiv.Perm.prodExtendRight a σ) x ≠ x)
  (x_1 : (Equiv.Perm.prodExtendRight a σ) ((Equiv.Perm.prodExtendRight a σ) x) ≠ (Equiv.Perm.prodExtendRight a σ) x),
  (∀ (a' : α) (b : β) (hab : (Equiv.Perm.prodExtendRight a σ) (a', b) ≠ (a', b))
      (x :
        (Equiv.Perm.prodExtendRight a σ) ((Equiv.Perm.prodExtendRight a σ) (a', b)) ≠
          (Equiv.Perm.prodExtendRight a σ) (a', b)),
      motive (a', b) hab x) →
    motive x hab x_1