Apply unknownprop_cad5bc2f5dac206bae20b714b49a2d836e36638f9959746bfb42cd8bf23be5ca with
omega,
prim4 omega,
False leaving 2 subgoals.
The subproof is completed by applying H0.
Let x0 of type ι → ι be given.
Apply form100_22_v3 with
x0.
Apply bij_surj with
omega,
prim4 omega,
x0.
The subproof is completed by applying H1.