Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Apply unknownprop_5c9f4155cb565ca5bafb78920a249f469cb73ce1ef22344ad5df255bab477655 with
bf68c.. x0 x1,
x2,
∃ x3 x4 : ι → ο . and (and (858ff.. x0 x3) (858ff.. x1 x4)) (x2 = 6e020.. 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 = 6e020.. x3 x4).
Apply unknownprop_951e3ef812229b5945a39a7fa79f4fd40c15277c7d728e18721eb777036d91be 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 FalseE with
x2 = c0709.. x5 x6 ⟶ ∃ x7 x8 : ι → ο . and (and (858ff.. x0 x7) (858ff.. x1 x8)) (x2 = 6e020.. x7 x8).
Apply unknownprop_856b8bfadc699ad231b4ff87ec1e03728d77f11011b06095d14ff77ccdcd01b1 with
x3,
x4,
x0,
x1.
Let x7 of type ι → ι → ο be given.
The subproof is completed by applying H3 with λ x8 x9 . x7 x9 x8.
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_432e2c1c265f7e33a9860d434376e8f246f661a5f0846be4ef608e5e6cdcb57b with
x0,
x1,
x3,
x4,
∃ x7 x8 : ι → ο . and (and (858ff.. x0 x7) (858ff.. x1 x8)) (x2 = 6e020.. 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 = 6e020.. 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.