Apply nat_complete_ind with λ x0 . 0 ∈ x0 ⟶ ∃ x1 . and (x1 ∈ omega) (∃ x2 : ι → ι . and (and (168aa.. prime_nat x1 x2) (05ecb.. x2 x1 = x0)) (∀ x3 . x3 ∈ omega ⟶ ∀ x4 : ι → ι . 168aa.. prime_nat x3 x4 ⟶ 05ecb.. x4 x3 = x0 ⟶ and (x3 = x1) (∀ x5 . x5 ∈ x1 ⟶ x4 x5 = x2 x5))).

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 . x1 ∈ x0 ⟶ 0 ∈ x1 ⟶ ∃ x2 . and (x2 ∈ omega) (∃ x3 : ι → ι . and (and (168aa.. prime_nat x2 x3) (05ecb.. x3 x2 = x1)) (∀ x4 . x4 ∈ omega ⟶ ∀ x5 : ι → ι . 168aa.. prime_nat x4 x5 ⟶ 05ecb.. x5 x4 = x1 ⟶ and (x4 = x2) (∀ x6 . x6 ∈ x2 ⟶ x5 x6 = x3 x6))).

Assume H2: 0 ∈ x0.

Apply xm with x0 = 1, ∃ x1 . and (x1 ∈ omega) (∃ x2 : ι → ι . and (and (168aa.. prime_nat x1 x2) (05ecb.. x2 x1 = x0)) (∀ x3 . x3 ∈ omega ⟶ ∀ x4 : ι → ι . 168aa.. prime_nat x3 x4 ⟶ 05ecb.. x4 x3 = x0 ⟶ and (x3 = x1) (∀ x5 . x5 ∈ x1 ⟶ x4 x5 = x2 x5))) leaving 2 subgoals.

Assume H3: x0 = 1.

Let x1 of type ο be given.

Assume H4: ∀ x2 . and (x2 ∈ omega) (∃ x3 : ι → ι . and (and (168aa.. prime_nat x2 x3) (05ecb.. x3 x2 = x0)) (∀ x4 . x4 ∈ omega ⟶ ∀ x5 : ι → ι . 168aa.. prime_nat x4 x5 ⟶ 05ecb.. x5 x4 = x0 ⟶ and (x4 = x2) (∀ x6 . x6 ∈ x2 ⟶ x5 x6 = x3 x6))) ⟶ x1.

Apply H4 with 0.

Apply andI with 0 ∈ omega, ∃ x2 : ι → ι . and (and (168aa.. prime_nat 0 x2) (05ecb.. x2 0 = x0)) (∀ x3 . x3 ∈ omega ⟶ ∀ x4 : ι → ι . 168aa.. prime_nat x3 x4 ⟶ 05ecb.. x4 x3 = x0 ⟶ and (x3 = 0) (∀ x5 . x5 ∈ 0 ⟶ x4 x5 = x2 x5)) leaving 2 subgoals.

Apply nat_p_omega with 0.

The subproof is completed by applying nat_0.

Let x2 of type ο be given.

Assume H5: ∀ x3 : ι → ι . and (and (168aa.. prime_nat 0 x3) (05ecb.. x3 0 = x0)) (∀ x4 . ... ⟶ ∀ x5 : ι → ι . ... ⟶ ... ⟶ and (x4 = 0) (∀ x6 . x6 ∈ 0 ⟶ x5 x6 = x3 x6)) ⟶ x2.

...

■

Proofgold Proof