proposition: Lemma isinclfromstn1 { X : UU } ( f : ⟦1⟧ -> X ) ( is : isaset X ) : isincl f.
proof: Proof. intros. apply ( isinclbetweensets f ( isasetstn 1 ) is ). intros x x' e. apply ( invmaponpathsweq weqstn1tounit x x' ( idpath tt ) ). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions