Let X, Tx and U be given.
Assume Hpara: paracompact_space X Tx.
Assume Hcover: open_cover X Tx U.
We will prove ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V.
We prove the intermediate claim Hforall: ∀U0 : set, open_cover X Tx U0 → ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U0.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U0 : set, open_cover X Tx U0 → ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U0) Hpara).
We prove the intermediate claim Hexists: ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U.
An exact proof term for the current goal is (Hforall U Hcover).
Apply Hexists to the current goal.
Let V be given.
Assume HV.
We use V to witness the existential quantifier.
An exact proof term for the current goal is (andEL (open_cover X Tx V ∧ locally_finite_family X Tx V) (refine_of V U) HV).
∎