Let x0 of type ι be given.
Apply unknownprop_da2bd49e935d53cfac7d2dade92fed0a4715f02a565c10e2712c01b04174bdd7 with
x0,
λ x1 x2 . Subq (aae7a.. x1 (f482f.. x0 (4ae4a.. 4a7ef..))) x0.
Apply unknownprop_fd8cfa9d525a4dec4072b8c89793bb3748a863e81655a11bd156798bb4989f99 with
x0,
λ x1 x2 . Subq (aae7a.. (e76d4.. x0) x1) x0.
The subproof is completed by applying unknownprop_aec23df2dd59da75ffdf3f91edcd7649ac84c5dc9e29603afda6a2c9b859aebd with x0.