Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1 ∈ x0.
Let x2 of type ι → ι be given.
Let x3 of type ι → ι be given.
Assume H1: ∀ x4 . x4 ∈ x0 ⟶ x2 x4 ∈ x0.
Let x4 of type ι → ι be given.
Assume H2: ∀ x5 . x5 ∈ x0 ⟶ x4 (x2 x5) = x3 (x4 x5).
Apply nat_ind with
λ x5 . x4 (1319b.. x5 x2 x1) = 1319b.. x5 x3 (x4 x1) leaving 2 subgoals.
Apply unknownprop_039fc83525f9619f7cfecb750766b6bca3d944a312bec3cbff47462eeab06c10 with
x2,
x1,
λ x5 x6 . x4 x6 = 1319b.. 0 x3 (x4 x1).
Apply unknownprop_039fc83525f9619f7cfecb750766b6bca3d944a312bec3cbff47462eeab06c10 with
x3,
x4 x1,
λ x5 x6 . x4 x1 = x6.
Let x5 of type ι → ι → ο be given.
Assume H3: x5 (x4 x1) (x4 x1).
The subproof is completed by applying H3.
Let x5 of type ι be given.
Apply unknownprop_002dbea24d6e2c65c6cefd906b209766da62711ebb920e89995e5f3cbbd95f66 with
x5,
x2,
x1,
λ x6 x7 . x4 x7 = 1319b.. (ordsucc x5) x3 (x4 x1) leaving 2 subgoals.
Apply nat_p_omega with
x5.
The subproof is completed by applying H3.
Apply unknownprop_002dbea24d6e2c65c6cefd906b209766da62711ebb920e89995e5f3cbbd95f66 with
x5,
x3,
x4 x1,
λ x6 x7 . x4 (x2 (1319b.. x5 x2 x1)) = x7 leaving 2 subgoals.
Apply nat_p_omega with
x5.
The subproof is completed by applying H3.
Apply H2 with
1319b.. x5 x2 x1,
λ x6 x7 . x7 = x3 (1319b.. x5 x3 (x4 x1)) leaving 2 subgoals.
Apply unknownprop_634dfe6db60252fae5fb11b99d8182640cd8d27dd5c6123b0e5c5ff1eb699c89 with
x0,
x1,
x2,
x5 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
set y6 to be
x3 (x4 (1319b.. x5 x2 x1))set y7 to be
x4 (1319b.. y6 x4 (x5 x2))Claim L5: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
Assume H5:
x8 (x5 (1319b.. y7 x5 (y6 x3))).
set y9 to be λ x9 . x8
Apply H4 with
λ x10 x11 . y9 (x5 x10) (x5 x11).
The subproof is completed by applying H5.
Let x8 of type ι → ι → ο be given.
Apply L5 with
λ x9 . x8 x9 y7 ⟶ x8 y7 x9.
Assume H6: x8 y7 y7.
The subproof is completed by applying H6.