Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Let x2 of type ι be given.
Apply H1 with
PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∃ x3 . and (prim1 x3 (4ae4a.. x2)) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4).
Apply unknownprop_279ca38e3c0e2b4f26dd5774d309c0af105ab029ebe30b2ac5354aa8f00721d3 with
x0,
x1,
x2,
∃ x3 . and (prim1 x3 (4ae4a.. x2)) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H7:
∃ x3 : ι → ο . 078b6.. x0 x1 x2 x3.
Apply H7 with
∃ x3 . and (prim1 x3 (4ae4a.. x2)) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4).
Let x3 of type ι → ο be given.
Apply H8 with
∃ x4 . and (prim1 x4 (4ae4a.. x2)) (∃ x5 : ι → ο . a59df.. x0 x1 x4 x5).
Apply H9 with
(∀ x4 : ι → ο . 8033b.. x0 x1 x2 x4 ⟶ PNoEq_ x2 x3 x4) ⟶ ∃ x4 . and (prim1 x4 (4ae4a.. x2)) (∃ x5 : ι → ο . a59df.. x0 x1 x4 x5).
Assume H12:
∀ x4 : ι → ο . 8033b.. x0 x1 x2 x4 ⟶ PNoEq_ x2 x3 x4.
Let x4 of type ο be given.
Apply H13 with
x2.
Apply andI with
prim1 x2 (4ae4a.. x2),
∃ x5 : ι → ο . a59df.. x0 x1 x2 x5 leaving 2 subgoals.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with x2.
Let x5 of type ο be given.
Assume H14:
∀ x6 : ι → ο . a59df.. x0 x1 x2 x6 ⟶ x5.
Apply H14 with
x3.
Apply unknownprop_b612bf4d512ad6227e8bff43683128e0125ebf717976bdcb0c23c328b2d194b7 with
x0,
x1,
x2,
x3 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H9.
Apply H7 with
∃ x3 . and (prim1 x3 (4ae4a.. x2)) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4).
Let x3 of type ι be given.
Assume H8:
(λ x4 . and (prim1 x4 x2) (∃ x5 : ι → ο . a59df.. x0 x1 x4 x5)) x3.
Apply H8 with
∃ x4 . and (prim1 x4 (4ae4a.. x2)) (∃ x5 : ι → ο . a59df.. x0 x1 x4 x5).
Assume H10:
∃ x4 : ι → ο . a59df.. x0 x1 x3 x4.
Let x4 of type ο be given.