| ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u8 = x8 |
|