Let X, Tx and U be given.

Assume H: partition_of_unity_dominated X Tx U.

An exact proof term for the current goal is (partition_of_unity_dominated_ex_family_pred X Tx U H).

∎