Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
x0,
cbf48.. x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_8e324a6fdc5dd93fc7954e55762c3ec235dc1a98306aca944193e8223699b282 with
x1.
The subproof is completed by applying H1.