proposition: Lemma predicateOnBaseConnectedType (X:PointedType) (b:isBaseConnected X) (P:X->hProp) (p:P (basepoint X)) : ∏ x, P x.
proof: Proof. intros x. apply (squash_to_hProp (b x)); intros e. now induction e. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions