Let alpha, p and q be given.

Assume H1.

Let R be given.

Assume H2.

Apply H1 to the current goal.

Let beta be given.

Assume H3.

Apply H3 to the current goal.

Assume H4: beta ∈ alpha.

Assume H5.

Apply H5 to the current goal.

Assume H5.

Apply H5 to the current goal.

Assume H6 H7 H8.

An exact proof term for the current goal is H2 beta H4 H6 H7 H8.

∎