----------------------------------------------------------------------------------------------------------------------------------------------------------------
Axiom of Extensionality

|- let a <- \d. (\e. d e) = d in a = \b. (\c. c) = \c. c

----------------------------------------------------------------------------------------------------------------------------------------------------------------
Axiom of Choice

|- let a <-
       \d.
        let e <-
            \g.
             (let h <- d g in
              \i.
               (let j <- h in
                \k. (\l. l j k) = \m. m ((\c. c) = \c. c) ((\c. c) = \c. c)) i <=>
               h) (d (select d)) in
        e = \f. (\c. c) = \c. c in
   a = \b. (\c. c) = \c. c

----------------------------------------------------------------------------------------------------------------------------------------------------------------
Axiom of Infinity

|- let a <-
       \p.
        (let h <-
             let q <-
                 \s.
                  let q <-
                      \t.
                       (let f <- p s = p t in
                        \g.
                         (let h <- f in
                          \i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
                         f) (s = t) in
                  q = \r. (\d. d) = \d. d in
             q = \r. (\d. d) = \d. d in
         \i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) (let u <-
                                                                           let q <-
                                                                               \v.
                                                                                let w <- \z. v = p z in
                                                                                let b <-
                                                                                    \x.
                                                                                     (let f <-
                                                                                          let q <-
                                                                                              \y.
                                                                                               (let f <- w y in
                                                                                                \g.
                                                                                                 (let h <- f in
                                                                                                  \i.
                                                                                                   (\j. j h i) =
                                                                                                   \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
                                                                                                 f) x in
                                                                                          q = \r. (\d. d) = \d. d in
                                                                                      \g.
                                                                                       (let h <- f in
                                                                                        \i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
                                                                                       f) x in
                                                                                b = \c. (\d. d) = \d. d in
                                                                           q = \r. (\d. d) = \d. d in
                                                                       (let f <- u in
                                                                        \g.
                                                                         (let h <- f in
                                                                          \i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
                                                                         f) (let b <- \d. d in b = \c. (\d. d) = \d. d)) in
   let b <-
       \e.
        (let f <-
             let l <-
                 \n.
                  (let f <- a n in
                   \g.
                    (let h <- f in
                     \i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
                    f) e in
             l = \m. (\d. d) = \d. d in
         \g.
          (let h <- f in
           \i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
          f) e in
   b = \c. (\d. d) = \d. d

----------------------------------------------------------------------------------------------------------------------------------------------------------------