proposition: Lemma predicateOnConnectedType {X:Type} (i : isConnected X) {P:X->hProp} (x0:X) (p:P x0) : ∏ x, P x.
proof: Proof. intros x. apply (squash_to_hProp (pr2 i x x0)); intros e. now induction e. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions