An exact proof term for the current goal is (ex32_4_regular_Lindelof_normal Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line_regular Sorgenfrey_line_Lindelof).