Unit : Type;
Unit = { unit };

Empty : Type;
Empty = { };

Bool : Type;
Bool = { true false };

T : Bool -> Type;
T = \ b -> case b of {
             true -> Unit
	   | false -> Empty };


Nat : Type;
Nat = (l : { z s }) * case l of {
                           z -> Unit
			 | s -> Rec [Nat] };

zero : Nat;
zero = ('z,'unit);

succ : Nat -> Nat;
succ = \ n -> ('s, fold n);

one : Nat;
one = succ zero;

two : Nat;
two = succ one;

add : Nat -> Nat -> Nat;
add = \ m n -> split m with (lm , m') ->
                 ! case lm of {
		     z -> [n]
 		   | s -> [succ (add (unfold m') n)] };

eqbNat : Nat -> Nat -> Bool;
eqbNat = \ m n -> split m with (lm , m') ->
                  split n with (ln , n') ->
                  ! case lm of {
		     z -> case ln of {
		             z -> ['true]
			   | s -> ['false] }
	           | s -> case ln of {
		             z -> ['false]
			   | s -> [eqbNat (unfold m') (unfold n')] } };

eqNat : Nat -> Nat -> Type;
eqNat = \ m n -> T (eqbNat m n);

reflNat : (n:Nat) -> eqNat n n;
reflNat = \ n -> split n with (ln , n') ->
       	        ! case ln of {
		     z -> ['unit]
		   | s -> [reflNat (unfold n')] };


Stream : Type -> Type;
Stream = \ a -> a * Rec [^ (Stream a)];

put : (a : Type) -> a -> Stream a -> Stream a;
put = \ a x xs -> (x, fold [xs]);

from : Nat -> Stream Nat;
from = \ n -> (n, fold [from (succ n)]);

tail : (a:Type) -> Stream a -> Stream a;
tail = \ a xs -> split xs with (x , xs') -> ! (unfold xs');

head : (a:Type) -> Stream a -> a;
head = \ a xs -> split xs with (x , xs') -> x;

map : (a : Type) -> (b : Type) -> (a -> b) -> Stream a -> Stream b;
map = \ a b f xs -> split xs with (x , xs') -> (f x, fold [map a b f (! (unfold xs'))]);

eqStream : (a : Type) -> (a -> a -> Type) -> Stream a -> Stream a -> Type;
eqStream = \ a eq xs ys ->
  split xs with (x , xs') ->
  split ys with (y , ys') ->
    eq x y * Rec [^ (eqStream a eq (! (unfold xs')) (! (unfold ys')))];

reflStream :  (a : Type) -> (eq : a -> a -> Type)
	   -> ((x : a) -> eq x x)
	   -> (xs : Stream a) -> eqStream a eq xs xs;
reflStream = \ a eq refl xs -> split xs with (x , xs') ->
	       	    	         (refl x, fold [reflStream a eq refl (! (unfold xs'))]);

lemma : (n : Nat) -> eqStream Nat eqNat (from (succ n))
                                        (map Nat Nat succ (from n));
lemma = \ n -> ((reflNat (succ n)), fold [lemma (succ n)]);