∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Nontrivial R]
  [NoZeroDivisors A] {ι : Type w} [Finite ι] {x : ι → A},
  AlgebraicIndependent R x → Algebra.trdeg R A ≤ Cardinal.mk ι → IsTranscendenceBasis R x