Let x0 of type ι be given.

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

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

Apply minus_SNo_0 with λ x1 x2 . lam 2 (λ x3 . If_i (x3 = 0) 0 x0) = lam 2 (λ x3 . If_i (x3 = 0) x2 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) (add_SNo (ap x2 0) (minus_SNo 1)) (ap x2 1))) (lam 2 (λ x2 . If_i (x2 = 0) 0 x0)) = lam 2 (λ x2 . If_i (x2 = 0) (minus_SNo x1) x0).

Apply unknownprop_002dbea24d6e2c65c6cefd906b209766da62711ebb920e89995e5f3cbbd95f66 with x1, λ x2 . lam 2 (λ x3 . If_i (x3 = 0) (add_SNo (ap x2 0) (minus_SNo 1)) (ap x2 1)), lam 2 (λ x2 . If_i (x2 = 0) 0 x0), λ x2 x3 . x3 = lam 2 (λ x4 . If_i (x4 = 0) (minus_SNo (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) (add_SNo (ap x3 0) (minus_SNo 1)) (ap x3 1)) = lam 2 (λ x4 . If_i (x4 = 0) (minus_SNo (ordsucc x1)) x0).

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

...

■

Proofgold Proof