Let x0 of type ι → ι be given.
Let x1 of type ι → ι be given.
Apply unknownprop_f4ff16b9b21fb43bec0dd0d2e94569d632f3d21b75932b9bcc0c1ffd4c0d62b6 with
236c6..,
prim1 x0,
236c6..,
prim1 x1,
x0 = x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_acde72e2f50237aebb3f280c9adbd840002728dc66b42dda2437acbece7fe515 with x0, x1.