Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_fd8cfa9d525a4dec4072b8c89793bb3748a863e81655a11bd156798bb4989f99 with
aae7a.. x0 x1,
λ x2 x3 . x2 = x1.
The subproof is completed by applying unknownprop_916f469d850241375b1e44b2c6308f0113078869ceee129c02712fae69c32a37 with x0, x1.