Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Let x3 of type ι be given.
Let x4 of type ι → ι → ι be given.
Apply explicit_Nats_E with
x0,
x1,
x2,
∀ x5 . prim1 x5 x0 ⟶ explicit_Nats_primrec x0 x1 x2 x3 x4 (x2 x5) = x4 x5 (explicit_Nats_primrec x0 x1 x2 x3 x4 x5).
Assume H3:
∀ x5 . prim1 x5 x0 ⟶ x2 x5 = x1 ⟶ ∀ x6 : ο . x6.
Assume H4:
∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 = x2 x6 ⟶ x5 = x6.
Assume H5:
∀ x5 : ι → ο . x5 x1 ⟶ (∀ x6 . x5 x6 ⟶ x5 (x2 x6)) ⟶ ∀ x6 . prim1 x6 x0 ⟶ x5 x6.
Let x5 of type ι be given.
Apply unknownprop_2611cf16ddfa1b4edb79e3ab7434c5739866f2053fe5690c0b558b5b0ae50bfd with
x0,
x1,
x2,
x3,
x4,
x5,
explicit_Nats_primrec x0 x1 x2 x3 x4 (x2 x5),
explicit_Nats_primrec x0 x1 x2 x3 x4 (x2 x5) = x4 x5 (explicit_Nats_primrec x0 x1 x2 x3 x4 x5) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
The subproof is completed by applying L8.
Let x6 of type ι be given.
Apply H9 with
explicit_Nats_primrec x0 x1 x2 x3 x4 (x2 x5) = x4 x5 (explicit_Nats_primrec x0 x1 x2 x3 x4 x5).
Assume H11:
a813b.. x0 x1 x2 x3 x4 x5 x6.
Apply H10 with
λ x7 x8 . x8 = x4 x5 (explicit_Nats_primrec x0 x1 x2 x3 x4 x5).
set y7 to be ...
Claim L12: ∀ x9 : ι → ο . x9 y8 ⟶ x9 y7
Let x9 of type ι → ο be given.
set y10 to be λ x10 . x9
Apply unknownprop_39f1d7e6fd5a8cac4be9227a915f550879579764a9e39ca1251d774dc53cc6ce with
x2,
x3,
x4,
x5,
x6,
y7,
y8,
explicit_Nats_primrec x2 x3 x4 x5 x6 y7,
λ x11 x12 . y10 (x6 y7 x11) (x6 y7 x12) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
The subproof is completed by applying H11.
The subproof is completed by applying L7.
The subproof is completed by applying H12.
Let x9 of type ι → ι → ο be given.
Apply L12 with
λ x10 . x9 x10 y8 ⟶ x9 y8 x10.
Assume H13: x9 y8 y8.
The subproof is completed by applying H13.