Let X, Tx, U and u be given.

Assume Hcov: open_cover X Tx U.

Assume HuU: u ∈ U.

We prove the intermediate claim Hop: ∀u0 : set, u0 ∈ U → u0 ∈ Tx.

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

An exact proof term for the current goal is (Hop u HuU).

∎