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.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_971065beceaddfb52e93ea203833e8996a97df3aa92f70259a8e3a2f800a69da with
x0,
x2,
x7,
x3,
x5,
x6 leaving 8 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H7.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x7,
x6,
λ x8 x9 . 099f3.. (bc82c.. x0 x5) x9 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x2,
x6,
λ x8 x9 . 099f3.. x9 (bc82c.. x3 x5) leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
The subproof is completed by applying H10.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x7,
x3 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H3.
Apply unknownprop_fb545b225a42993d98e0d062b6c9208b8321e87814f4e26de3418c134068c2c8 with
bc82c.. x0 (bc82c.. x1 x2),
bc82c.. x7 (bc82c.. x3 x1),
bc82c.. x3 x4 leaving 5 subgoals.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x0,
bc82c.. x1 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x7,
bc82c.. x3 x1 leaving 2 subgoals.
The subproof is completed by applying H7.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x3,
x1 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x1,
x2,
λ x8 x9 . 099f3.. (bc82c.. x0 x9) (bc82c.. x7 (bc82c.. x3 x1)) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with
x0,
x2,
x1,
λ x8 x9 . 099f3.. x9 (bc82c.. x7 (bc82c.. x3 x1)) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with
x7,
x3,
x1,
λ x8 x9 . 099f3.. (bc82c.. (bc82c.. x0 x2) x1) x9 leaving 4 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
Apply unknownprop_b751afd4b96b439a72771c5e6447c46f37e6851a11a9a372baaf45b11a370b67 with
bc82c.. x0 x2,
x1,
bc82c.. x7 x3 leaving 4 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying H1.
The subproof is completed by applying L13.
The subproof is completed by applying L11.
Apply unknownprop_4e34a620b1f5496f1d776caaa0190761feb7cd3a7f3cd78c34f9288c12df6d94 with
x3,
x1,
x7,
λ x8 x9 . 099f3.. x8 (bc82c.. x3 x4) leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
The subproof is completed by applying H7.
Apply unknownprop_50ea7279d1527aec8642473c7707da12238935f258091dd2df6f6eae075c74e1 with
x3,
bc82c.. x1 x7,
x4 leaving 4 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x1,
x7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H7.
The subproof is completed by applying H4.
The subproof is completed by applying H9.