Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_2dabdcbdf62eb35e893b1da7cf9ea26462f4b63bcb37cf7a3640d2d2117f04a1 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_2dabdcbdf62eb35e893b1da7cf9ea26462f4b63bcb37cf7a3640d2d2117f04a1 with
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Apply L4 with
λ x3 x4 . 099f3.. x3 x2.
Apply L5 with
λ x3 x4 . 099f3.. (bc82c.. (bc82c.. x0 x1) (f4dc0.. x1)) x3.
Apply unknownprop_b751afd4b96b439a72771c5e6447c46f37e6851a11a9a372baaf45b11a370b67 with
bc82c.. x0 x1,
f4dc0.. x1,
bc82c.. x2 x1 leaving 4 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_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
x1.
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.
The subproof is completed by applying H3.