Eq : (a:Type) -> a -> a -> Type;
Eq = \ a x y -> (P : a -> Type) -> P x -> P y;

refl : (a:Type) -> (x:a) -> Eq a x x;
refl = \ a x P px -> px;

Stream : Type;
Stream = (tag : {Cons}) * case tag of {Cons -> [^Stream] };

ticks : Stream;
ticks = ('Cons, [ticks]);

l1 : Eq Stream ticks ('Cons, [ticks]);
l1 = refl Stream ticks;

l2 : (s : Stream) -> (t : Stream) -> (Eq Stream s t)
                 -> Eq Stream ('Cons, [s]) ('Cons, [t]);
l2 = \ s t q P p -> q (\ x -> P ('Cons,[x])) p;

{- bad error message! -}

{- unbox x with [y] -> t 

   |- C : Type
   |- x : ^A
   y:A, x==[y] |- t : C
   -----------------------------
   |- unbox x with [y] -> t : C

   unbox [a] with [y] -> t ==> let y=a in t


   ![a] = a

-}

{-
l3 : (A:Type) -> (a:A) -> (b:A) -> Eq A a b -> Eq (^A) [a] [b];
-}