:l Bool.pi

andb' : Bool -> Bool -> Bool;
andb' = \ b c -> case c of {
                  true -> b
                | false -> 'false };

inftyOpt : Type -> Bool -> Type
   = \ A b -> case b of {
                 true -> A
               | false -> ^ A };

boxOpt : (b:Bool) -> (A:Type) -> A -> inftyOpt A b
       = \ b A a -> case b of { true -> a
		              | false -> [a] };

forceOpt : (b:Bool) -> (A:Type) -> inftyOpt A b -> A 
       = \ b A a -> case b of { true -> a
		              | false -> !a };

Tok : Type;

P : Bool -> Type
  = \ b -> (l : { fail empty sat alt seq } ) *
           case l of {
             fail -> EqBool 'false b
           | empty -> EqBool 'true b
           | sat -> (Tok -> Bool) * (EqBool 'false b)
           | alt -> (n1 n2 : Bool) * Rec [P n1] * Rec [P n2] * (EqBool (orb n1 n2) b)
           | seq -> (n1 n2 : Bool) * inftyOpt (Rec [P n1]) n2 *
                                     inftyOpt (Rec [P n2]) n1 * (EqBool (andb' n1 n2) b) };


star : P 'false -> P 'true;
plus : P 'false -> P 'false;

star = \ p -> ('alt , ('true, ('false, (fold ('empty, reflBool 'true),
                                       (fold (plus p),
                                       reflBool 'false)))));

plus = \ p -> ('seq, ('false, ('true, (fold p, ([fold (star p)], reflBool 'false)) )) );