proposition: Lemma isasetterm {σ: signature} (s: sorts σ): isaset (term σ s).
proof: Proof. apply isaset_total2. - apply isasetoplist. - intros. apply isasetaprop. apply isasetstack. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Combinatorics.Maybe UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Signatures