Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: 09364.. x0 = 09364.. x1.

Apply unknownprop_220466dabb9c90c9b087796465f1368ac3c1e9d1ef55643ebed4c27316fb8803 with x0, λ x2 x3 . x2 = x1.

Apply unknownprop_220466dabb9c90c9b087796465f1368ac3c1e9d1ef55643ebed4c27316fb8803 with x1, λ x2 x3 . 158d3.. (09364.. x0) = x2.

Apply H0 with λ x2 x3 . 158d3.. x3 = 158d3.. (09364.. x1).

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

Assume H1: x2 (158d3.. (09364.. x1)) (158d3.. (09364.. x1)).

The subproof is completed by applying H1.

■

Proofgold Proof