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