Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
In x1 x0,
x1 = x0.
Apply unknownprop_0a3ac46e7c6819fed4662428384c6a352add25246833c8a02444013e6de47ec3 with
x0,
x1.
The subproof is completed by applying H0.