set y0 to be ...
set y1 to be ...
Apply functional extensionality with
λ x2 . (λ x3 . ∀ x4 . nat_p x4) x2 ⟶ ∀ x3 . In x3 x2 ⟶ ∃ x4 . (∃ x5 . and (Subq x5 x4) (∃ x6 . and (exactly2 (binrep (Power (Power (Power 0))) 0)) (not (atleast4 (Power 0))))) ⟶ ∀ x5 . atleast5 (Union 0) ⟶ atleast4 x4,
λ x2 . (∀ x3 . nat_p x3) ⟶ ∀ x3 . In x3 x2 ⟶ ∃ x4 . (∃ x5 . and (Subq x5 x4) (∃ x6 . and (exactly2 (binrep (Power (Power (Power 0))) 0)) (not (atleast4 (Power 0))))) ⟶ ∀ x5 . atleast5 (Union 0) ⟶ atleast4 x4,
λ x2 x3 : ι → ο . y1 x2,
λ x2 x3 : ο . y1 x2 leaving 3 subgoals.
Let x2 of type ι be given.
set y4 to be
λ x4 : ο . (λ x5 x6 : ο . x5 ⟶ x6) ((λ x5 . ∀ x6 . nat_p x6) x2) = (λ x5 x6 : ο . x5 ⟶ x6) x4set y5 to be λ x5 x6 : ο . y4 x5
Claim L0:
y5 ((λ x6 . ∀ x7 . nat_p x7) x2) ((λ x6 . ∀ x7 . nat_p x7) x2)Let x6 of type (ο → ο) → (ο → ο) → ο be given.
Assume H0:
x6 ((λ x7 x8 : ο . x7 ⟶ x8) ((λ x7 . ∀ x8 . nat_p x8) y4)) ((λ x7 x8 : ο . x7 ⟶ x8) ((λ x7 . ∀ x8 . nat_p x8) y4)).
The subproof is completed by applying H0.
Apply L0 with
λ x6 x7 : ο → ο . y5 x6.
Let x6 of type ο → ο → ο be given.
The subproof is completed by applying H1.