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 Hleft2 _.

Apply Hleft2 to the current goal.

Assume Hleft3 _.

Apply Hleft3 to the current goal.

Assume Hleft4 _.

Apply Hleft4 to the current goal.

Assume _ HB.

An exact proof term for the current goal is HB.

∎