----------------------------------------------------------------------------------------------------------------------------------------------------------------
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

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