An exact proof term for the current goal is (andER (topology_on X Tx ∧ open_cover X Tx U) (∃P : set, partition_of_unity_family X Tx U P) H).