Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply unknownprop_4e34a620b1f5496f1d776caaa0190761feb7cd3a7f3cd78c34f9288c12df6d94 with
x0,
x4,
x1,
λ x5 x6 . 099f3.. x6 (bc82c.. x2 (bc82c.. x3 x4)) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H1.
Apply unknownprop_eadcd59c0d09fed06457bbc8bc4ca8c6803a6d350a2f946a8d7abb7dc0d0e94b with
x1,
x0,
x2,
x3,
x4 leaving 6 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.