theorem
proved
singularEdgePath_homotopicRel_const_of_loop_winding_zero
show as:
singularEdgePath_homotopicRel_const_of_loop_winding_zero