instance PiBase.instInjPathConnectedSpaceOfPrepathConnectedSpace {X : Type u_1} [TopologicalSpace X] [h : InjPathConnectedSpace X] : PrepathConnectedSpace X

theorem PiBase.Formal.T39 : P38 ≤ P37