{α : Sort u_1} →
  {motive : FinEnum α → Sort u} →
    (t : FinEnum α) →
      ((card : ℕ) →
          (equiv : α ≃ Fin card) → [decEq : DecidableEq α] → motive { card := card, equiv := equiv, decEq := decEq }) →
        motive t