∀ {F : Type u_1} [inst : CommSemiring F] {f : Polynomial F} (hf : Polynomial.HasSeparableContraction 1 f)
  (motive : (∃ m, hf.degree * 1 ^ m = f.natDegree) → Prop) (x : ∃ m, hf.degree * 1 ^ m = f.natDegree),
  (∀ (a : ℕ) (ha : hf.degree * 1 ^ a = f.natDegree), motive ⋯) → motive x