Let x0 of type ι be given.

Assume H0: x0 ∈ omega.

Let x1 of type ι be given.

Let x2 of type ι be given.

Apply unknownprop_0cf9d41e7d60a71e427c4cc0ec2fef6270f645a1c8d9f615ee0ec90cdcdc2a5f with λ x3 . x2, λ x3 . λ x4 : ι → ι . λ x5 . 4ec03.. (ap x5 0) (x4 (stream_rest x5)), x0, λ x3 x4 : ι → ι . x4 x1 = 4ec03.. (ap x1 0) (b38a5.. x0 (stream_rest x1) x2) leaving 2 subgoals.

Apply omega_nat_p with x0.

The subproof is completed by applying H0.

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

Assume H1: x3 ((λ x4 . λ x5 : ι → ι . λ x6 . 4ec03.. (ap x6 0) (x5 (stream_rest x6))) x0 (nat_primrec_ii (λ x4 . x2) (λ x4 . λ x5 : ι → ι . λ x6 . 4ec03.. (ap x6 0) (x5 (stream_rest x6))) x0) x1) (4ec03.. (ap x1 0) (b38a5.. x0 (stream_rest x1) x2)).

The subproof is completed by applying H1.

■

Proofgold Proof