Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H4:
not (x0 = x1).
Assume H5:
not (x0 = x2).
Assume H6:
not (x0 = x3).
Assume H7:
not (x1 = x2).
Assume H8:
not (x1 = x3).
Assume H9:
not (x2 = x3).
Apply unknownprop_50049cb08ded1102cafef929946d9c8ea6123047d68bb1e4e7608faddaa0e3b3 with
4,
λ x4 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) x4 leaving 3 subgoals.
Apply unknownprop_077979b790f9097ea9250573e60509ec9410103c35a67e0558983ee18582fb09 with
3.
Apply unknownprop_077979b790f9097ea9250573e60509ec9410103c35a67e0558983ee18582fb09 with
2.
The subproof is completed by applying unknownprop_d97d6922f54612bc34684069408098060ad6c1b04a8b4fda7efccfad8c5e25b7.
Let x4 of type ι be given.
Apply unknownprop_0fadd198c09f8629cb4c152d61d82c413244246b3c85763ebe3d75aeff28b65a with
x4,
λ x5 . In (ap (lam 4 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 x3)))) x5) 4 leaving 5 subgoals.
The subproof is completed by applying H10.
Apply unknownprop_36e12e654911209cf6139dcce25eccbb5fde1b810c75c2e7ca0621b0951e30f5 with
x0,
x1,
x2,
x3,
λ x5 x6 . In x6 4.
The subproof is completed by applying H0.
Apply unknownprop_b4d9b28ffdfc26091f8308714bc32dda459f8ef72e65f6991a681b771ecda216 with
x0,
x1,
x2,
x3,
λ x5 x6 . In x6 4.
The subproof is completed by applying H1.
Apply unknownprop_cd1658f3a72c6a2bb94a2daab3e8270dc8dd343e6dd52f56f65d81dc131b0875 with
x0,
x1,
x2,
x3,
λ x5 x6 . In x6 4.
The subproof is completed by applying H2.
Apply unknownprop_23cea816b4176293b3d8ba4787692b8cb93e0a3eae6b638b0967d563a0bdc507 with
x0,
x1,
x2,
x3,
λ x5 x6 . In x6 4.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply unknownprop_0fadd198c09f8629cb4c152d61d82c413244246b3c85763ebe3d75aeff28b65a with
x4,
λ x6 . ap (lam 4 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 x3)))) x6 = ap (lam 4 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 x3)))) x5 ⟶ x6 = x5 leaving 5 subgoals.
The subproof is completed by applying H10.
Apply unknownprop_0fadd198c09f8629cb4c152d61d82c413244246b3c85763ebe3d75aeff28b65a with
x5,
λ x6 . ap (lam 4 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 x3)))) 0 = ap (lam 4 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 x3)))) x6 ⟶ 0 = x6 leaving 5 subgoals.
The subproof is completed by applying H11.
Assume H12:
ap (lam 4 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 x3)))) 0 = ap (lam 4 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) ... ...)))) 0.