Apply unknownprop_aca6546ca70975227cfdd401f01c6af1ee4084a6127606b8f15131e520646158 with
λ x0 x1 x2 . ∀ x3 x4 : ι → ο . 858ff.. x1 x3 ⟶ 858ff.. x2 x4 ⟶ ∀ x5 x6 . x3 x5 ⟶ d7d78.. x0 x5 x6 ⟶ x4 x6 leaving 9 subgoals.
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.
Assume H3: x1 x3.
Claim L5: x1 = x2
Apply unknownprop_117be7573c60b7d0abaafc299d87847fec12e93691ef0a29fced62dc7418d130 with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Claim L6: x3 = x4
Apply unknownprop_ae1e79e1a2bccfe8aebcb1e813103c4afd5b26690657ff2ca9061fbf87b7bf35 with
x3,
x4.
The subproof is completed by applying H4.
Apply L5 with
λ x5 x6 : ι → ο . x5 x4.
Apply L6 with
λ x5 x6 . x1 x5.
The subproof is completed by applying H3.
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.
Assume H1:
∀ x5 x6 : ι → ο . 858ff.. x0 x5 ⟶ 858ff.. x1 x6 ⟶ ∀ x7 x8 . x5 x7 ⟶ d7d78.. x3 x7 x8 ⟶ x6 x8.
Assume H3:
∀ x5 x6 : ι → ο . 858ff.. x1 x5 ⟶ 858ff.. x2 x6 ⟶ ∀ x7 x8 . x5 x7 ⟶ d7d78.. x4 x7 x8 ⟶ x6 x8.
Let x5 of type ι → ο be given.
Let x6 of type ι → ο be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Assume H6: x5 x7.
Apply unknownprop_cff582124c579af9c23894076366d9c1d4be330d88106ca325a9ffd28cc0a5c6 with
x3,
x4,
x7,
x8.
The subproof is completed by applying H7.
Apply L8 with
x6 x8.
Let x9 of type ι be given.
Apply H9 with
x6 x8.
Apply unknownprop_ba62a7b985827e5b6d2adfd88e1946699da89cb2c580e048e15cbf1151f093ec with
x3,
x0,
x1,
x6 x8 leaving 2 subgoals.
The subproof is completed by applying H0.
Claim L14:
∃ x10 : ι → ο . 858ff.. x1 x10
Apply unknownprop_7bb51105313454d4aa8c466e57e3cafc9a19eebc0a8b69682b3e7f6ddfb8275a with
x1.
The subproof is completed by applying H13.
Apply L14 with
x6 x8.
Let x10 of type ι → ο be given.
Claim L16: x10 x9
Apply H1 with
x5,
x10,
x7,
x9 leaving 4 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H15.
The subproof is completed by applying H6.
The subproof is completed by applying H10.
Apply H3 with
x10,
x6,
x9,
x8 leaving 4 subgoals.
The subproof is completed by applying H15.
The subproof is completed by applying H5.
The subproof is completed by applying L16.
The subproof is completed by applying H11.
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.
Assume H3: x1 x3.
Apply unknownprop_117be7573c60b7d0abaafc299d87847fec12e93691ef0a29fced62dc7418d130 with
5e331..,
x2,
07017.. leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_fecdd5feecd0903be897193dc6d5c928cc89dee8ad0003c049becc2b40bb6fd9.
Apply L5 with
λ x5 x6 : ι → ο . x6 x4.
Apply unknownprop_11ab5ad84446dc0c8599e250d04348a580b4e461b777edde7bd671068dfc2d3a with
x3,
x4.
The subproof is completed by applying H4.
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.