An exact proof term for the current goal is (andEL (C ⊆ X) (∃U ∈ T, C = X ∖ U) (closed_in_package X T C HC)).