# TODO: this stinks
and := λ(: lctx TContext)(: rctx TContext). (: (
   (match (Tuple( lctx rctx )) (
      ()
      ( (Tuple( TCtxEOF _ )) (set lctx TCtxEOF) )
      ( (Tuple( _ TCtxEOF )) (set lctx TCtxEOF) )
      ( _ (
         (set lctx (union( lctx rctx )))
      ))
   ))
   lctx
) TContext);

and := λ(: lt Type)(: rt Type). (: (
   (let tt (TAnd( (close lt) (close rt) )))
   tt
) Type);