Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Apply unknownprop_5c9f4155cb565ca5bafb78920a249f469cb73ce1ef22344ad5df255bab477655 with
a3eb9.. x0 x1,
x2,
∃ x3 x4 : ι → ο . and (and (858ff.. x0 x3) (858ff.. x1 x4)) (x2 = c0709.. x3 x4) leaving 4 subgoals.
The subproof is completed by applying H0.
Apply FalseE with
x2 = 07017.. ⟶ ∃ x3 x4 : ι → ο . and (and (858ff.. x0 x3) (858ff.. x1 x4)) (x2 = c0709.. x3 x4).
Apply unknownprop_112da44b75efcdc251767c8f8619fc43c6b883afd5ac71e5854bf36b62571f0c with
x0,
x1.
Let x3 of type ι → ι → ο be given.
The subproof is completed by applying H1 with λ x4 x5 . x3 x5 x4.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι → ο be given.
Let x6 of type ι → ο be given.
Apply unknownprop_1f81fbea8647063ecd1729d03bf27a5327e4a018cc4ad3e99f64b38027811c93 with
x0,
x1,
x3,
x4,
∃ x7 x8 : ι → ο . and (and (858ff.. x0 x7) (858ff.. x1 x8)) (x2 = c0709.. x7 x8) leaving 2 subgoals.
The subproof is completed by applying H3.
Assume H5: x0 = x3.
Assume H6: x1 = x4.
Let x7 of type ο be given.
Apply H7 with
x5.
Let x8 of type ο be given.
Apply H8 with
x6.
Apply and3I with
858ff.. x0 x5,
858ff.. x1 x6,
x2 = c0709.. x5 x6 leaving 3 subgoals.
Apply H5 with
λ x9 x10 . 858ff.. x10 x5.
The subproof is completed by applying H1.
Apply H6 with
λ x9 x10 . 858ff.. x10 x6.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι → ο be given.
Let x6 of type ι → ο be given.
Apply FalseE with
x2 = 6e020.. x5 x6 ⟶ ∃ x7 x8 : ι → ο . and (and (858ff.. x0 x7) (858ff.. x1 x8)) (x2 = c0709.. x7 x8).
Apply unknownprop_856b8bfadc699ad231b4ff87ec1e03728d77f11011b06095d14ff77ccdcd01b1 with
x0,
x1,
x3,
x4.
The subproof is completed by applying H3.