Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_da1ac74e7171cfbc42378617a62cb62f2a4d8bf3a5c1e029c4b4e4f12cda8627 with
x0,
λ x2 x3 . prim1 (09364.. x1) x3.
Apply unknownprop_e4d6e0bfb4ef6d52ee13edd54a77c8cc7f0a3af8ffb1b8da66d4f98842dd28b5 with
91630.. 4a7ef..,
94f9e.. x0 (λ x2 . 09364.. x2),
09364.. x1.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with
x0,
09364..,
x1.
The subproof is completed by applying H0.