Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_0b5b61a66a1ed2eb843dbce5c5f6930c63a284fe5e33704d9f0cc564310ec40b with
94f9e.. x0 (λ x3 . f6917.. x3),
94f9e.. x1 (λ x3 . 09364.. x3),
f6917.. x2.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with
x0,
f6917..,
x2.
The subproof is completed by applying H0.