Let X and Tx be given.

Assume Hreg: regular_space X Tx.

Assume HL: Lindelof_space X Tx.

We prove the intermediate claim HH: Hausdorff_space X Tx.

An exact proof term for the current goal is (regular_space_implies_Hausdorff X Tx Hreg).

We prove the intermediate claim Hpara: paracompact_space X Tx.

An exact proof term for the current goal is (regular_Lindelof_paracompact X Tx Hreg HL).

An exact proof term for the current goal is (paracompact_Hausdorff_normal X Tx Hpara HH).

∎