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_5f01c21b20f5151eb58230694adfaac0cd3dc9203ea975568057400d5e0e5f7a 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_785de96e0736c15754c7d7b1a8c7a8a67f701ffa3e6f8320bf2fa437af385e9c 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.