Let α, p and q be given.

Assume H1.

Let R be given.

Assume H2.

Apply H1 to the current goal.

Let β be given.

Assume H3.

Apply H3 to the current goal.

Assume H4: β ∈ α.

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 β H4 H6 H7 H8.

∎