Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι → ι → ι be given.

Let x3 of type ι → ι → ι be given.

Let x4 of type ι → ι → ο be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H0: x0 = pack_b_b_r_e_e x1 x2 x3 x4 x5 x6.

Apply H0 with λ x7 x8 . x6 = ap x8 5.

Let x7 of type ι → ι → ο be given.

The subproof is completed by applying tuple_6_5_eq with x1, encode_b x1 x2, encode_b x1 x3, encode_r x1 x4, x5, x6, λ x8 x9 . x7 x9 x8.

■

Proofgold Proof