Let x, y, X, Y, Z, W, U and U' be given.

Assume HUE HU'I1 HU'I2.

Let u be given.

Assume Hu: u ∈ U.

Apply HUE u Hu to the current goal.

Let w be given.

Assume Hw.

Let z be given.

Assume Hz Huwz.

rewrite the current goal using Huwz (from left to right).

Apply HU'I1 to the current goal.

An exact proof term for the current goal is Hw.

An exact proof term for the current goal is Hz.

Let w be given.

Assume Hw.

Let z be given.

Assume Hz Huwz.

rewrite the current goal using Huwz (from left to right).

Apply HU'I2 to the current goal.

An exact proof term for the current goal is Hw.

An exact proof term for the current goal is Hz.

∎