Let X and B be given.

Assume H: basis_on X B.

Set A to be the term B ⊆ 𝒫 X.

Set Bcov to be the term (∀x ∈ X, ∃b ∈ B, x ∈ b).

Set Bref to be the term (∀b1 ∈ B, ∀b2 ∈ B, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2).

We prove the intermediate claim Hab: A ∧ Bcov.

An exact proof term for the current goal is (andEL (A ∧ Bcov) Bref H).

An exact proof term for the current goal is (andER A Bcov Hab).

∎