Let X, Tx, U and P be given.

Assume HP: partition_of_unity_family X Tx U P.

Apply HP to the current goal.

Assume _ HF.

An exact proof term for the current goal is HF.

∎