Let x0 of type ι → ο be given.
Assume H0: ∃ x1 . x0 x1.
Let x1 of type ο be given.
Assume H1:
∀ x2 . and (x0 x2) (∀ x3 . x0 x3 ⟶ ZermeloWO x2 x3) ⟶ x1.
Apply H1 with
prim0 ((λ x2 : ι → ο . Descr_Vo1 (λ x3 : ι → ο . and ((λ x4 : ι → ο . ∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . x5 x6 ⟶ x5 ((λ x7 : ι → ο . λ x8 . and (x7 x8) (x8 = prim0 (λ x9 . x7 x9) ⟶ ∀ x9 : ο . x9)) x6)) ⟶ (∀ x6 : (ι → ο) → ο . (∀ x7 : ι → ο . x6 x7 ⟶ x5 x7) ⟶ x5 (Descr_Vo1 x6)) ⟶ x5 x4) x3) (∀ x4 . x2 x4 ⟶ x3 x4))) x0).
Apply andI with
x0 (prim0 ((λ x2 : ι → ο . Descr_Vo1 (λ x3 : ι → ο . and ((λ x4 : ι → ο . ∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . x5 x6 ⟶ x5 ((λ x7 : ι → ο . λ x8 . and (x7 x8) (x8 = prim0 (λ x9 . x7 x9) ⟶ ∀ x9 : ο . x9)) x6)) ⟶ (∀ x6 : (ι → ο) → ο . (∀ x7 : ι → ο . x6 x7 ⟶ x5 x7) ⟶ x5 (Descr_Vo1 x6)) ⟶ x5 x4) x3) (∀ x4 . x2 x4 ⟶ x3 x4))) x0)),
∀ x2 . x0 x2 ⟶ ZermeloWO (prim0 ((λ x3 : ι → ο . Descr_Vo1 (λ x4 : ι → ο . and ((λ x5 : ι → ο . ∀ x6 : (ι → ο) → ο . (∀ x7 : ι → ο . x6 x7 ⟶ x6 ((λ x8 : ι → ο . λ x9 . and (x8 x9) (x9 = prim0 (λ x10 . x8 x10) ⟶ ∀ x10 : ο . x10)) x7)) ⟶ (∀ x7 : (ι → ο) → ο . (∀ x8 : ι → ο . x7 x8 ⟶ x6 x8) ⟶ x6 (Descr_Vo1 x7)) ⟶ x6 x5) x4) (∀ x5 . x3 x5 ⟶ x4 x5))) x0)) x2 leaving 2 subgoals.
Apply unknownprop_e010b3a19747f7c1717c62914b4ab66c3d63ab0bd9893159907133d88739bd12 with
x0.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H2: x0 x2.
Let x3 of type ι → ο be given.
Assume H3:
and ((λ x4 : ι → ο . ∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . x5 x6 ⟶ x5 ((λ x7 : ι → ο . λ x8 . and (x7 x8) (x8 = prim0 (λ x9 . x7 x9) ⟶ ∀ x9 : ο . x9)) x6)) ⟶ (∀ x6 : (ι → ο) → ο . (∀ x7 : ι → ο . x6 x7 ⟶ x5 x7) ⟶ x5 (Descr_Vo1 x6)) ⟶ x5 x4) x3) (∀ x4 . x4 = prim0 ((λ x5 : ι → ο . Descr_Vo1 (λ x6 : ι → ο . and ((λ x7 : ι → ο . ∀ x8 : (ι → ο) → ο . (∀ x9 : ι → ο . x8 x9 ⟶ x8 ((λ x10 : ι → ο . λ x11 . and (x10 x11) (x11 = prim0 (λ x12 . x10 x12) ⟶ ∀ x12 : ο . x12)) x9)) ⟶ (∀ x9 : (ι → ο) → ο . (∀ x10 : ι → ο . x9 x10 ⟶ x8 x10) ⟶ x8 (Descr_Vo1 x9)) ⟶ x8 x7) x6) (∀ x7 . x5 x7 ⟶ x6 x7))) x0) ⟶ x3 x4).
Apply H3 with
x3 x2.
Assume H4:
(λ x4 : ι → ο . ∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . ... ⟶ x5 ...) ⟶ (∀ x6 : (ι → ο) → ο . (∀ x7 : ι → ο . x6 x7 ⟶ x5 x7) ⟶ x5 (Descr_Vo1 x6)) ⟶ x5 x4) ....