Let α, β, p and q be given.

Assume H1.

Let R be given.

Assume HC1 HC2 HC3.

Apply H1 to the current goal.

Assume H1.

Apply H1 to the current goal.

An exact proof term for the current goal is HC1.

Assume H1.

Apply H1 to the current goal.

Assume H1.

Apply H1 to the current goal.

An exact proof term for the current goal is HC2.

Assume H1.

Apply H1 to the current goal.

Assume H1.

Apply H1 to the current goal.

An exact proof term for the current goal is HC3.

∎