proposition: Lemma seqsonisaset ( A : hSet ) : isaset ( seqson A ).
proof: Proof. intros. unfold seqson. change ( isofhlevel 2 ( nat -> A ) ). apply impredfun. apply (pr2 A). Defined.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers