An exact proof term for the current goal is (andEL (topology_on X Tx) (∀Fam : set, open_cover_of X Tx Fam → has_finite_subcover X Tx Fam) H).