{α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] →
      {g : Equiv.Perm α} →
        {motive : g.Basis → Sort u} →
          (t : g.Basis) →
            ((toFun : ↥g.cycleFactorsFinset → α) →
                (mem_support_self' : ∀ (c : ↥g.cycleFactorsFinset), toFun c ∈ (↑c).support) →
                  motive { toFun := toFun, mem_support_self' := mem_support_self' }) →
              motive t