Lemma predicateOnBaseConnectedType (X:PointedType) (b:isBaseConnected X) (P:X->hProp) (p:P (basepoint X)) : ∏ x, P x. Proof. intros x. apply (squash_to_hProp (b x)); intros e. now induction e. Defined.