Let X, Tx and W be given.

Assume Hnorm: normal_space X Tx.

Assume Hcov: open_cover X Tx W.

Assume Hlf: locally_finite_family X Tx W.

An exact proof term for the current goal is (normal_locally_finite_partition_of_unity_family_rec X Tx W Hnorm Hcov Hlf).

∎