proposition: Lemma BasePointComponent_isincl {X:PointedType} : isincl (@basePointComponent_inclusion X).
proof: Proof. use isinclpr1. intros x. apply propproperty. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions