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:
∀ x4 . x4 ∈ x0 ⟶ x3 (ap x1 x4) = x3 (ap x2 x4).
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply H1 with
λ x6 x7 . x3 x6 = x3 x7 leaving 4 subgoals.
The subproof is completed by applying H0.
Let x6 of type ι be given.
Let x7 of type ι → ι → ο be given.
Assume H2: x7 (x3 x6) (x3 x6).
The subproof is completed by applying H2.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H2: x3 x6 = x3 x7.
Let x8 of type ι → ι → ο be given.
The subproof is completed by applying H2 with λ x9 x10 . x8 x10 x9.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Assume H2: x3 x6 = x3 x7.
Assume H3: x3 x7 = x3 x8.
set y9 to be x3 x6
set y10 to be x4 y9
Claim L4: ∀ x11 : ι → ο . x11 y10 ⟶ x11 y9
Let x11 of type ι → ο be given.
Assume H4: x11 (x5 y10).
Apply H2 with
λ x12 . x11.
Apply H3 with
λ x12 . x11.
The subproof is completed by applying H4.
Let x11 of type ι → ι → ο be given.
Apply L4 with
λ x12 . x11 x12 y10 ⟶ x11 y10 x12.
Assume H5: x11 y10 y10.
The subproof is completed by applying H5.