Let x0 of type ι be given.

Apply nat_ind with λ x1 . 1319b.. x1 (λ x2 . lam 2 (λ x3 . If_i (x3 = 0) (ordsucc (ap x2 0)) (ap x2 1))) (lam 2 (λ x2 . If_i (x2 = 0) 0 x0)) = lam 2 (λ x2 . If_i (x2 = 0) x1 x0) leaving 2 subgoals.

Apply unknownprop_039fc83525f9619f7cfecb750766b6bca3d944a312bec3cbff47462eeab06c10 with λ x1 . lam 2 (λ x2 . If_i (x2 = 0) (ordsucc (ap x1 0)) (ap x1 1)), lam 2 (λ x1 . If_i (x1 = 0) 0 x0), λ x1 x2 . x2 = lam 2 (λ x3 . If_i (x3 = 0) 0 x0).

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

Assume H0: x1 (lam 2 (λ x2 . If_i (x2 = 0) 0 x0)) (lam 2 (λ x2 . If_i (x2 = 0) 0 x0)).

The subproof is completed by applying H0.

Let x1 of type ι be given.

Assume H0: nat_p x1.

Assume H1: 1319b.. x1 (λ x2 . lam 2 (λ x3 . If_i (x3 = 0) (ordsucc (ap x2 0)) (ap x2 1))) (lam 2 (λ x2 . If_i (x2 = 0) 0 x0)) = lam 2 (λ x2 . If_i (x2 = 0) x1 x0).

Apply unknownprop_002dbea24d6e2c65c6cefd906b209766da62711ebb920e89995e5f3cbbd95f66 with x1, λ x2 . lam 2 (λ x3 . If_i (x3 = 0) (ordsucc (ap x2 0)) (ap x2 1)), lam 2 (λ x2 . If_i (x2 = 0) 0 x0), λ x2 x3 . x3 = lam 2 (λ x4 . If_i (x4 = 0) (ordsucc x1) x0) leaving 2 subgoals.

Apply nat_p_omega with x1.

The subproof is completed by applying H0.

Apply H1 with λ x2 x3 . lam 2 (λ x4 . If_i (x4 = 0) (ordsucc (ap x3 0)) (ap x3 1)) = lam 2 (λ x4 . If_i (x4 = 0) (ordsucc x1) x0).

Apply tuple_2_0_eq with x1, x0, λ x2 x3 . lam 2 (λ x4 . If_i (x4 = 0) (ordsucc x3) (ap (lam 2 (λ x5 . If_i (x5 = 0) x1 x0)) 1)) = lam 2 (λ x4 . If_i (x4 = 0) (ordsucc x1) x0).

Apply tuple_2_1_eq with x1, x0, λ x2 x3 . lam 2 (λ x4 . If_i (x4 = 0) (ordsucc x1) x3) = lam 2 (λ x4 . If_i (x4 = 0) (ordsucc x1) x0).

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

Assume H2: x2 (lam 2 (λ x3 . If_i (x3 = 0) (ordsucc x1) x0)) ....

...

■

Proofgold Proof