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