Let X, Tx and U be given.
Assume H: partition_of_unity_dominated X Tx U.
We prove the intermediate claim HUcov: open_cover X Tx U.
An exact proof term for the current goal is (andER (topology_on X Tx) (open_cover X Tx U) (partition_of_unity_dominated_topology_open_cover X Tx U H)).
An exact proof term for the current goal is (andER (∀u : set, u ∈ U → u ∈ Tx) (covers X U) HUcov).
∎