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