instance PiBase.instLocallyPathConnectedSpaceOfLocallyInjPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [h : LocallyInjPathConnectedSpace X] : LocallyPathConnectedSpace X

theorem PiBase.Formal.T63 : P43 ≤ P42