∀ {α : Type} [inst : Mul α] [inst_1 : AddMonoid α]
  {motive : (a : ℕ) → {ds : List ℕ} → (a_1 : Holor α ds) → Holor.CPRankMax a a_1 → Prop} {a : ℕ} {ds : List ℕ}
  {a_1 : Holor α ds} (t : Holor.CPRankMax a a_1),
  (∀ {ds : List ℕ}, motive 0 0 ⋯) →
    (∀ (n : ℕ) {ds : List ℕ} (x y : Holor α ds) (a : x.CPRankMax1) (a_2 : Holor.CPRankMax n y),
        motive (n + 1) (x + y) ⋯) →
      motive a a_1 t