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_ind with
x0,
x1,
x2,
λ x5 . ∀ x6 x7 . a813b.. x0 x1 x2 x3 x4 x5 x6 ⟶ a813b.. x0 x1 x2 x3 x4 x5 x7 ⟶ x6 = x7 leaving 3 subgoals.
The subproof is completed by applying H0.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H1:
a813b.. x0 x1 x2 x3 x4 x1 x5.
Assume H2:
a813b.. x0 x1 x2 x3 x4 x1 x6.
Apply unknownprop_987d3840aa104d50ea50759bc446be3aae0e33c59dc8291c7942424d9287e6ed with
x0,
x1,
x2,
x3,
x4,
x6,
λ x7 x8 . x5 = x8 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_987d3840aa104d50ea50759bc446be3aae0e33c59dc8291c7942424d9287e6ed with
x0,
x1,
x2,
x3,
x4,
x5 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x5 of type ι be given.
Assume H2:
∀ x6 x7 . a813b.. x0 x1 x2 x3 x4 x5 x6 ⟶ a813b.. x0 x1 x2 x3 x4 x5 x7 ⟶ x6 = x7.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H3:
a813b.. x0 x1 x2 x3 x4 (x2 x5) x6.
Assume H4:
a813b.. x0 x1 x2 x3 x4 (x2 x5) x7.
Apply unknownprop_2611cf16ddfa1b4edb79e3ab7434c5739866f2053fe5690c0b558b5b0ae50bfd with
x0,
x1,
x2,
x3,
x4,
x5,
x6,
x6 = x7 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Let x8 of type ι be given.
Assume H5:
(λ x9 . and (x6 = x4 x5 x9) (a813b.. x0 x1 x2 x3 x4 x5 x9)) x8.
Apply H5 with
x6 = x7.
Assume H6: x6 = x4 x5 x8.
Assume H7:
a813b.. x0 x1 x2 x3 x4 x5 x8.
Apply unknownprop_2611cf16ddfa1b4edb79e3ab7434c5739866f2053fe5690c0b558b5b0ae50bfd with
x0,
x1,
x2,
x3,
x4,
x5,
x7,
x6 = x7 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
Let x9 of type ι be given.
Assume H8:
(λ x10 . and (x7 = x4 x5 x10) (a813b.. x0 x1 x2 x3 x4 x5 x10)) x9.
Apply H8 with
x6 = x7.
Assume H9: x7 = x4 x5 x9.
Assume H10:
a813b.. x0 x1 x2 x3 x4 x5 x9.
Apply H6 with
λ x10 x11 . x11 = x7.
Apply H9 with
λ x10 x11 . x4 x5 x8 = x11.
set y10 to be x4 x5 x8
set y11 to be x5 x6 y10
Claim L11: ∀ x12 : ι → ο . x12 y11 ⟶ x12 y10
Let x12 of type ι → ο be given.
Assume H11: x12 (x6 x7 y11).
set y13 to be λ x13 . x12
Apply H2 with
y10,
y11,
λ x14 x15 . y13 (x6 x7 x14) (x6 x7 x15) leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Let x12 of type ι → ι → ο be given.
Apply L11 with
λ x13 . x12 x13 y11 ⟶ x12 y11 x13.
Assume H12: x12 y11 y11.
The subproof is completed by applying H12.