Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Apply unknownprop_f4ff16b9b21fb43bec0dd0d2e94569d632f3d21b75932b9bcc0c1ffd4c0d62b6 with
236c6..,
prim0 x0 x1,
236c6..,
prim1 x2,
∀ x3 : ο . x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_4c7c6a01193a68b8e5840b3e04313713b98b7f4e59d0d80bcd9a29ba93e073e2 with x0, x1, x2.