[chewxy]

Scott encoding even has a weirder implications (if you're not used to it) if you think about it

    0 ≡ λf.λx.x
    1 ≡ λf.λx.x (λf.λx.x)
    2 ≡ λf.λx.x (λf.λx.x (λf.λx.x))

Or if you allow meta variables in your expression:

    0 ≡ λf.λx.x
    1 ≡ λf.λx.x 0
    2 ≡ λf.λx.x 1

This implies 2 contains 1, 1 contains 0. Bam. Scott encoding also encodes some parts of set theory.

Following from this, of course, all ADTs can be encoded following the Scott encoding scheme.