Let A be given.

We will prove refines_cover A A.

Let U be given.

Assume HU: U ∈ A.

We use U to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HU.

An exact proof term for the current goal is (Subq_ref U).

∎