Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: x3 ∈ setexp x1 x0.

Let x4 of type ι be given.

Assume H1: x4 ∈ setexp x2 x1.

Apply lam_Pi with x0, λ x5 . x2, λ x5 . ap x4 (ap x3 x5).

Let x5 of type ι be given.

Assume H2: x5 ∈ x0.

Apply ap_Pi with x1, λ x6 . x2, x4, ap x3 x5 leaving 2 subgoals.

The subproof is completed by applying H1.

Apply ap_Pi with x0, λ x6 . x1, x3, x5 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H2.

■

Proofgold Proof