fact: Definition vsignature (σ : signature) (V: varspec σ): signature := make_signature (sorts σ) (setcoprod (names σ) V) (sumofmaps (ar σ) (λ v, nil ,, varsort v)).
imports: UniMath.Foundations.All UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Terms