Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_544f4d34085c39fe852eae7f16fd7fa4f1aacc16d23d4ca0f8649dd632a3ab3b with
a0628.. x0 (a0628.. x1 x2),
a0628.. (a0628.. x0 x1) x2 leaving 4 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
set y3 to be ...
set y4 to be ...
Claim L7: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Apply unknownprop_9d7a134423d1f17ac48e0d0adf872beb67ffd28835aafce6857803caa53395b8 with
x2,
a0628.. y3 y4,
λ x6 . x5 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
set y6 to be ...
set y7 to be ...
Claim L8: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
set y9 to be ...
set y10 to be ...
Claim L9: ∀ x11 : ι → ο . x11 y10 ⟶ x11 y9
Let x11 of type ι → ο be given.
Apply f_eq_i with
λ x12 . add_SNo (28f8d.. y6) x12,
28f8d.. (a0628.. y7 x8),
add_SNo (28f8d.. y7) (28f8d.. x8),
λ x12 . x11 leaving 2 subgoals.
Apply unknownprop_9d7a134423d1f17ac48e0d0adf872beb67ffd28835aafce6857803caa53395b8 with
y7,
x8 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
set y12 to be ...
set y13 to be ...
Claim L10: ∀ x14 : ι → ο . x14 y13 ⟶ x14 y12
Let x14 of type ι → ο be given.
Apply add_SNo_assoc with
28f8d.. x8,
28f8d.. y9,
28f8d.. y10,
λ x15 . x14 leaving 4 subgoals.
Apply unknownprop_62ffbce17a1080b510b3d10f88e78f4b8e9088a2c54409ce0c70e91f74a9fd08 with
x8.
The subproof is completed by applying H0.
Apply unknownprop_62ffbce17a1080b510b3d10f88e78f4b8e9088a2c54409ce0c70e91f74a9fd08 with
y9.
The subproof is completed by applying H1.
Apply unknownprop_62ffbce17a1080b510b3d10f88e78f4b8e9088a2c54409ce0c70e91f74a9fd08 with
y10.
The subproof is completed by applying H2.
set y15 to be ...
Claim L11: ∀ x18 : ι → ο . x18 y17 ⟶ x18 y16
Let x18 of type ι → ο be given.
set y19 to be λ x19 . x18
Apply unknownprop_9d7a134423d1f17ac48e0d0adf872beb67ffd28835aafce6857803caa53395b8 with
y10,
x11,
λ x20 x21 . y19 ((λ x22 . add_SNo x22 (28f8d.. y12)) x20) ((λ x22 . add_SNo x22 (28f8d.. y12)) x21) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H11.
set y18 to be λ x18 x19 . y17 x19 x18
Apply L11 with
λ x19 . y18 x19 y17 ⟶ y18 y17 x19 leaving 2 subgoals.
Assume H12: y18 y17 y17.
The subproof is completed by applying H12.
The subproof is completed by applying L11.
set y14 to be λ x14 . y13
Apply L10 with
λ x15 . y14 x15 y13 ⟶ y14 y13 x15 leaving 2 subgoals.
Assume H11: y14 y13 y13.
The subproof is completed by applying H11.
The subproof is completed by applying L10.
set y11 to be λ x11 . y10
Apply L9 with
λ x12 . y11 x12 y10 ⟶ y11 y10 x12 leaving 2 subgoals.
Assume H10: y11 y10 y10.
The subproof is completed by applying H10.
set y12 to be λ x12 . y11
Apply unknownprop_9d7a134423d1f17ac48e0d0adf872beb67ffd28835aafce6857803caa53395b8 with
a0628.. y7 x8,
y9,
λ x13 x14 . y12 x14 x13 leaving 3 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L3.
The subproof is completed by applying L9.
set y8 to be λ x8 . y7
Apply L8 with
λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H9: y8 y7 y7.
The subproof is completed by applying H9.
The subproof is completed by applying L8.
Let x5 of type ι → ι → ο be given.
Apply L7 with
λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H8: x5 y4 y4.
The subproof is completed by applying H8.