List :: * -> *;
List e = forall (listT::*) . listT -> (e->listT->listT) -> listT;

Nil :: forall (e::*) . List e;
Nil e = \ (listT::*) (nil::listT) (cons::e->listT->listT) -> nil;

Cons :: forall (e::*) . e -> List e -> List e;
Cons e x xs = \ (listT::*) (nil::listT) (cons::e->listT->listT) -> cons x (xs listT nil cons);

foldr :: forall (a::*) (b::*) . (a->b->b) -> b -> List a -> b;
foldr a b f z xs = xs b z f;

foldl :: forall (a::*) (b::*) . (b->a->b) -> b -> List a -> b;
foldl a b f z xs = foldr a (b->b) (\ (x::a) (g::b->b) (v::b) -> g (f v x)) (\ (x::b) -> x) xs z;

map :: forall (a::*) (b::*) . (a->b) -> List a -> List b;
map a b f xs = foldr a (List b) (\ (x::a) (r::List b) -> Cons b (f x) r) (Nil b) xs;

append :: forall (a::*) . List a -> List a -> List a;
append a xs ys = foldr a (List a) (Cons a) ys xs;

reverse :: forall (a::*) . List a -> List a;
reverse a xs = foldl a (List a) (\ (r :: List a) (x :: a) -> Cons a x r) (Nil a) xs;