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 unknownprop_3f1c52242e03407c3c59c0f336ed065f2350324861a03fb92c84a367e3866d05 with
x0,
x1,
x2,
x3,
λ x5 x6 . In x5 (setexp x4 4).
Apply unknownprop_9cbe1b438cb309fdaf3dcacebb3b572a10a17828098a582be8e9441d5a1eab25 with
λ x5 x6 : ι → ι → ι . In (lam 4 (ap (lam 4 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 x3)))))) (x6 x4 4).
Apply unknownprop_ae7ff6762664969563026849f911ad347655d2dee93f3e04751eb40cfcd41ed9 with
4,
λ x5 . x4,
λ x5 . ap (lam 4 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 x3)))) x5.
Let x5 of type ι be given.
Apply unknownprop_0fadd198c09f8629cb4c152d61d82c413244246b3c85763ebe3d75aeff28b65a with
x5,
λ x6 . In (ap (lam 4 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 x3)))) x6) x4 leaving 5 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_36e12e654911209cf6139dcce25eccbb5fde1b810c75c2e7ca0621b0951e30f5 with
x0,
x1,
x2,
x3,
λ x6 x7 . In x7 x4.
The subproof is completed by applying H0.
Apply unknownprop_b4d9b28ffdfc26091f8308714bc32dda459f8ef72e65f6991a681b771ecda216 with
x0,
x1,
x2,
x3,
λ x6 x7 . In x7 x4.
The subproof is completed by applying H1.
Apply unknownprop_cd1658f3a72c6a2bb94a2daab3e8270dc8dd343e6dd52f56f65d81dc131b0875 with
x0,
x1,
x2,
x3,
λ x6 x7 . In x7 x4.
The subproof is completed by applying H2.
Apply unknownprop_23cea816b4176293b3d8ba4787692b8cb93e0a3eae6b638b0967d563a0bdc507 with
x0,
x1,
x2,
x3,
λ x6 x7 . In x7 x4.
The subproof is completed by applying H3.