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