+Booleans, Church numerals, and v3 lists in OCaml
+------------------------------------------------
+
+(These questions adapted from web materials by Umut Acar. See
+<http://www.mpi-sws.org/~umut/>.)
+
+Let's think about the encodings of booleans, numerals and lists in System F,
+and get data-structures with the same form working in OCaml. (Of course, OCaml
+has *native* versions of these datas-structures: its `true`, `1`, and `[1;2;3]`.
+But the point of our exercise requires that we ignore those.)
+
+Recall from class System F, or the polymorphic λ-calculus.
+
+ types τ ::= c | 'a | τ1 → τ2 | ∀'a. τ
+ expressions e ::= x | λx:τ. e | e1 e2 | Λ'a. e | e [τ]
+
+The boolean type, and its two values, may be encoded as follows:
+
+ bool := ∀'a. 'a → 'a → 'a
+ true := Λ'a. λt:'a. λf :'a. t
+ false := Λ'a. λt:'a. λf :'a. f
+
+It's used like this: