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.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Let x9 of type ι be given.
Let x10 of type ι be given.
Let x11 of type ι be given.
Let x12 of type ι be given.
Let x13 of type ι be given.
Let x14 of type ι be given.
Let x15 of type ι be given.
Let x16 of type ι be given.
Let x17 of type ι be given.
Let x18 of type ι be given.
Let x19 of type ι be given.
Let x20 of type ι be given.
Let x21 of type ι be given.
Let x22 of type ι be given.
Let x23 of type ι be given.
Let x24 of type ι be given.
Apply unknownprop_cac7df4246a157059a70fd105054822672ca5b092a1d2bd109bb504b890345cf with
lam 5 (λ x25 . If_i (x25 = 0) x0 (If_i (x25 = 1) x1 (If_i (x25 = 2) x2 (If_i (x25 = 3) x3 x4)))),
lam 5 (λ x25 . If_i (x25 = 0) x5 (If_i (x25 = 1) x6 (If_i (x25 = 2) x7 (If_i (x25 = 3) x8 x9)))),
lam 5 (λ x25 . If_i (x25 = 0) x10 (If_i (x25 = 1) x11 (If_i (x25 = 2) x12 (If_i (x25 = 3) x13 x14)))),
lam 5 (λ x25 . If_i (x25 = 0) x15 (If_i (x25 = 1) x16 (If_i (x25 = 2) x17 (If_i (x25 = 3) x18 x19)))),
lam 5 (λ x25 . If_i (x25 = 0) x20 (If_i (x25 = 1) x21 (If_i (x25 = 2) x22 (If_i (x25 = 3) x23 x24)))),
λ x25 x26 . ap x26 4 = x9.
The subproof is completed by applying unknownprop_137195276c7cf95441e7b83c8306414f9b3b996c1bc95c04d52e171fd6d5474a with x5, x6, x7, x8, x9.