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.
Apply unknownprop_36f11cc7571fa2487251d5a7c42936b64e63f594759a4c4f588173d9cd2aec53 with
bc82c.. x0 x1,
bc82c.. x4 x5,
bc82c.. x2 x3 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_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x4,
x5 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
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_30c79c0e02402151cd3152635d98c753ad546bc3a622bfa516c8603d0e4e28fb with
x0,
x1,
x4,
x5,
λ x6 x7 . 099f3.. x7 (bc82c.. (bc82c.. x2 x3) (bc82c.. x4 x5)) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with
x2,
x3,
bc82c.. x4 x5,
λ x6 x7 . x6 = bc82c.. (bc82c.. x2 x5) (bc82c.. x3 x4) leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x4,
x5 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with
x2,
x5,
bc82c.. x3 x4,
λ x6 x7 . bc82c.. x2 (bc82c.. x3 (bc82c.. x4 x5)) = x6 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Claim L8: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
set y9 to be λ x9 . x8
Apply unknownprop_4e34a620b1f5496f1d776caaa0190761feb7cd3a7f3cd78c34f9288c12df6d94 with
x5,
y6,
y7,
λ x10 x11 . y9 (bc82c.. x4 x10) (bc82c.. x4 x11) leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H8.
Let x8 of type ι → ι → ο be given.
Apply L8 with
λ x9 . x8 x9 y7 ⟶ x8 y7 x9.
Assume H9: x8 y7 y7.
The subproof is completed by applying H9.
Apply L8 with
λ x6 x7 . 099f3.. (bc82c.. (bc82c.. x0 x4) (bc82c.. x1 x5)) x7.
Apply unknownprop_05217a7ee3979c752afdb6976b4b09416f9f3c51faced83e1d8281aef2596f24 with
bc82c.. x0 x4,
bc82c.. x1 x5,
bc82c.. x2 x5,
bc82c.. x3 x4 leaving 6 subgoals.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x0,
x4 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x1,
x5 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x2,
x5 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
The subproof is completed by applying H7.