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 Hleft _.
Apply Hleft to the current goal.
Assume _ HE.
An exact proof term for the current goal is HE.
∎