Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Let x2 of type ι be given.
Apply H0 with
PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ι → ο . 8033b.. x0 x1 x2 x3 ⟶ 8033b.. x0 x1 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)).
Let x3 of type ι → ο be given.
Apply H5 with
8033b.. x0 x1 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)).
Apply andI with
6f2c4.. x0 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)),
dafc2.. x1 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)) leaving 2 subgoals.
Let x4 of type ι be given.
Let x5 of type ι → ο be given.
Apply H11 with
40dde.. x4 x5 (4ae4a.. x2) (λ x6 . and (x3 x6) (x6 = x2 ⟶ ∀ x7 : ο . x7)).
Let x6 of type ι be given.
Apply H13 with
40dde.. x4 x5 (4ae4a.. x2) (λ x7 . and (x3 x7) (x7 = x2 ⟶ ∀ x8 : ο . x8)).
Assume H15:
∃ x7 : ι → ο . and (x0 x6 x7) (35b9b.. x4 x5 x6 x7).
Apply H15 with
40dde.. x4 x5 (4ae4a.. x2) (λ x7 . and (x3 x7) (x7 = x2 ⟶ ∀ x8 : ο . x8)).
Let x7 of type ι → ο be given.
Assume H16:
(λ x8 : ι → ο . and (x0 x6 x8) (35b9b.. x4 x5 x6 x8)) x7.
Apply H16 with
40dde.. x4 x5 (4ae4a.. x2) (λ x8 . and (x3 x8) (x8 = x2 ⟶ ∀ x9 : ο . x9)).
Assume H17: x0 x6 x7.
Apply unknownprop_81ad141295a808fea0b45ad277e31915f7577f7fce50f799a6434a1b613c1ee0 with
x4,
x6,
4ae4a.. x2,
x5,
x7,
λ x8 . and (x3 x8) (x8 = x2 ⟶ ∀ x9 : ο . x9) leaving 5 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying H14.
The subproof is completed by applying L8.
The subproof is completed by applying H18.
Apply unknownprop_73b6444bcb1b9cb998566f55e286e78644e785a99d955b3281cf269899ab486c with
x6,
4ae4a.. x2,
x7,
λ x8 . and (x3 x8) (x8 = x2 ⟶ ∀ x9 : ο . x9),
40dde.. x6 x7 (4ae4a.. x2) (λ x8 . and (x3 x8) (x8 = x2 ⟶ ∀ x9 : ο . x9)) leaving 4 subgoals.