∀ (R : Type u_1) {X : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {F₁ F₂ : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A},
  (∀ (x : X), F₁ (FreeNonUnitalNonAssocAlgebra.of R x) = F₂ (FreeNonUnitalNonAssocAlgebra.of R x)) → F₁ = F₂