Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_01059785170d3f6ee7ccae83a53df10446a7c0a3edc3b8aae06f45756a2928c3 with
bc82c.. x0 x1,
bc82c.. x2 x1,
bc82c.. x2 x3 leaving 5 subgoals.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_7a8a09f739ce2b80076d5abc4f8aa49cc67deae8353a3a5f1876e1562db9a7cf with
x0,
x1,
x2 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Apply unknownprop_50ea7279d1527aec8642473c7707da12238935f258091dd2df6f6eae075c74e1 with
x2,
x1,
x3 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H5.