proposition: Lemma iscontr_sfuntosunit {S: UU} {X: sUU S}: iscontr (X s→ sunit S).
proof: Proof. apply impred_iscontr. intros. apply iscontrfuntounit. Defined.
imports: UniMath.Foundations.All UniMath.Combinatorics.MoreLists UniMath.Algebra.Universal.HVectors