proposition: Theorem isinclfromunit {X : UU} (f : unit -> X) (is : isaset X) : isincl f.
proof: Proof. intros. apply (isinclbetweensets f (isofhlevelcontr 2 (iscontrunit)) is). intros. induction x. induction x'. apply idpath. Defined.
imports: UniMath.Foundations.PartA