Nat = ∀α::*.α → (α → α) → α;

zero = Λα::*.λz:α.λs:α → α.z;

succ = λn:Nat.Λα::*.λz:α.λs:α → α.s (n [α] z s);

add = λm:Nat.λn:Nat.m [Nat] n succ;

List = λα::*.∀φ::*⇒*.φ α → (α → φ α → φ α) → φ α;

nil = Λα::*.Λφ::*⇒*.λnil:φ α.λcons:α → φ α → φ α.nil;

cons = Λα::*.λx:α.λxs:List α.
         Λφ::*⇒*.λnil:φ α.λcons:α → φ α → φ α.
             cons x (xs [φ] nil cons);

foldList = Λα::*.Λβ::*.
        λc:α → β → β.λn:β.λl:List α.
           l [λγ::*.β] n c;

append = Λα::*.
          λl:List α.λr:List α.
            foldList [α] [List α] (cons [α]) l r;

reverse = Λα::*.
          λl:List α.
            foldList [α] [List α → List α]
              (λx:α. λk:List α → List α. λxs: List α. k (cons [α] x xs))
              (λxs: List α. xs) l (nil [α]);

Option = λα::*.∀φ::*⇒*.φ α → (α → φ α) → φ α;

none = Λα::*.Λφ::*⇒*.λnone:φ α.λsome:α → φ α.none;

some = Λα::*.λx:α.
         Λφ::*⇒*.λnone:φ α.λsome:α → φ α.
             some x;

foldOption = Λα::*.Λβ::*.
        λs:α → β.λn:β.λo:Option α.
           o [λγ::*.β] n s;

### Question 3 ###

# TTree = ...

# empty = ...

# tree = ...

# foldTTree = ...

# totalNatTree : TTree Nat → Nat = ...

### Question 4 ###

# queue = ...
