fact: Definition free_algebra (σ: signature) (V: varspec σ): algebra σ := @make_algebra σ (termset σ V) build_term.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.VTerms