∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  {motive : (a : E) → IsSolvableByRad F a → Prop},
  (∀ (α : F), motive ((algebraMap F E) α) ⋯) →
    (∀ (α β : E) (a : IsSolvableByRad F α) (a_1 : IsSolvableByRad F β), motive α a → motive β a_1 → motive (α + β) ⋯) →
      (∀ (α : E) (a : IsSolvableByRad F α), motive α a → motive (-α) ⋯) →
        (∀ (α β : E) (a : IsSolvableByRad F α) (a_1 : IsSolvableByRad F β),
            motive α a → motive β a_1 → motive (α * β) ⋯) →
          (∀ (α : E) (a : IsSolvableByRad F α), motive α a → motive α⁻¹ ⋯) →
            (∀ (α : E) (n : ℕ) (hn : n ≠ 0) (a : IsSolvableByRad F (α ^ n)), motive (α ^ n) a → motive α ⋯) →
              ∀ {a : E} (t : IsSolvableByRad F a), motive a t