Let A, B and C be given.

Assume HCB: refines_cover C B.

Assume HBA: refines_cover B A.

We will prove refines_cover C A.

Let U be given.

Assume HU: U ∈ C.

We prove the intermediate claim HexV: ∃V : set, V ∈ B ∧ U ⊆ V.

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

Apply HexV to the current goal.

Let V be given.

Assume HVpair.

We prove the intermediate claim HVB: V ∈ B.

An exact proof term for the current goal is (andEL (V ∈ B) (U ⊆ V) HVpair).

We prove the intermediate claim HUV: U ⊆ V.

An exact proof term for the current goal is (andER (V ∈ B) (U ⊆ V) HVpair).

We prove the intermediate claim HexW: ∃W : set, W ∈ A ∧ V ⊆ W.

An exact proof term for the current goal is (HBA V HVB).

Apply HexW to the current goal.

Let W be given.

Assume HWpair.

We prove the intermediate claim HWA: W ∈ A.

An exact proof term for the current goal is (andEL (W ∈ A) (V ⊆ W) HWpair).

We prove the intermediate claim HVW: V ⊆ W.

An exact proof term for the current goal is (andER (W ∈ A) (V ⊆ W) HWpair).

We use W to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HWA.

An exact proof term for the current goal is (Subq_tra U V W HUV HVW).

∎