An exact proof term for the current goal is (andER (∀u0 : set, u0 ∈ U → u0 ∈ Tx) (covers X U) Hcov).