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_13b99fd000490b330591961fc1e419c9f4ce9013dd2d43edb6af3c0a8dc957a3 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_b751afd4b96b439a72771c5e6447c46f37e6851a11a9a372baaf45b11a370b67 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.