Let X, Tx and W be given.
Assume Hnorm: normal_space X Tx.
Assume HWcov: open_cover X Tx W.
Assume HWlf: locally_finite_family X Tx W.
An exact proof term for the current goal is (normal_locally_finite_open_cover_shrinking_rec X Tx W Hnorm HWcov HWlf).
∎