Let U, V and W be given.

Assume HWV: refine_of W V.

Assume HVU: refine_of V U.

We will prove refine_of W U.

Let w be given.

Assume HwW: w ∈ W.

Apply (HWV w HwW) to the current goal.

Let v be given.

Assume Hv: v ∈ V ∧ w ⊆ v.

We prove the intermediate claim HvV: v ∈ V.

An exact proof term for the current goal is (andEL (v ∈ V) (w ⊆ v) Hv).

We prove the intermediate claim Hwsubv: w ⊆ v.

An exact proof term for the current goal is (andER (v ∈ V) (w ⊆ v) Hv).

Apply (HVU v HvV) to the current goal.

Let u be given.

Assume Hu: u ∈ U ∧ v ⊆ u.

We use u to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (u ∈ U) (v ⊆ u) Hu).

An exact proof term for the current goal is (Subq_tra w v u Hwsubv (andER (u ∈ U) (v ⊆ u) Hu)).

∎