Let x0 of type ι be given.

Assume H0: even_nat x0.

Apply H0 with divides_nat 2 x0.

Assume H1: x0 ∈ omega.

Assume H2: ∃ x1 . and (x1 ∈ omega) (x0 = mul_nat 2 x1).

Apply H2 with divides_nat 2 x0.

Let x1 of type ι be given.

Assume H3: (λ x2 . and (x2 ∈ omega) (x0 = mul_nat 2 x2)) x1.

Apply H3 with divides_nat 2 x0.

Assume H4: x1 ∈ omega.

Assume H5: x0 = mul_nat 2 x1.

Apply and3I with 2 ∈ omega, x0 ∈ omega, ∃ x2 . and (x2 ∈ omega) (mul_nat 2 x2 = x0) leaving 3 subgoals.

Apply nat_p_omega with 2.

The subproof is completed by applying nat_2.

The subproof is completed by applying H1.

Let x2 of type ο be given.

Assume H6: ∀ x3 . and (x3 ∈ omega) (mul_nat 2 x3 = x0) ⟶ x2.

Apply H6 with x1.

Apply andI with x1 ∈ omega, mul_nat 2 x1 = x0 leaving 2 subgoals.

The subproof is completed by applying H4.

Let x3 of type ι → ι → ο be given.

The subproof is completed by applying H5 with λ x4 x5 . x3 x5 x4.

■

Proofgold Proof