substitute := λ(: tctx TContext)(: tt List<Type>). (: (
   (match tt (
      ()
      ( LEOF () )
      ( (LCons( par rst )) (
         (set tt (cons(
            (substitute( tctx par ))
            (substitute( tctx rst ))
         )))
      ))
   ))
   tt
) List<Type>);

substitute := λ(: tctx TContext)(: tt Type). (: (
   (match tt (
      ()
      ( (TVar v) (
         (while (non-zero tctx) (match tctx (
            ()
            ( TCtxNil (set tctx TCtxEOF) )
            ( (TCtxBind( rst tk tv _ )) (
               (if (==( tk v )) (
                  (set tt tv)
                  (set tctx TCtxEOF)
               ) (set tctx rst))
            ))
         )))
      ))
      ( (TGround( tag pars )) (
         (set tt (TGround(
            tag
            (close(substitute( tctx pars )))
         )))
      ))
      ( (TAnd( lt rt )) (
         (set tt (TAnd(
            (close(substitute( tctx lt )))
            (close(substitute( tctx rt )))
         )))
      ))
      ( _ () )
   ))
   tt
) Type);

substitute := λ(: tctx Context)(: tt List<Type>). (: (
   (match tt (
      ()
      ( LEOF () )
      ( (LCons( par rst )) (
         (set tt (cons(
            (substitute( tctx par ))
            (substitute( tctx rst ))
         )))
      ))
   ))
   tt
) List<Type>);

substitute := λ(: tctx Context)(: tt Type). (: (
   (match tt (
      ()
      ( (TVar v) (
         (while (non-zero tctx) (match tctx (
            ()
            ( CtxNil (set tctx CtxEOF) )
            ( (CtxBind( rst tk (Lit( tv _ )) )) (
               (if (==( tk v )) (
                  (set tt (parse-type tv))
                  (set tctx CtxEOF)
               ) (set tctx rst))
            ))
            ( (CtxBind( rst tk (Var( tv _ )) )) (
               (if (==( tk v )) (
                  (set tt (parse-type tv))
                  (set tctx CtxEOF)
               ) (set tctx rst))
            ))
            ( (CtxBind( rst tk tv )) (
               (set tctx rst)
            ))
         )))
      ))
      ( (TGround( tag pars )) (
         (set tt (TGround(
            tag
            (close(substitute( tctx pars )))
         )))
      ))
      ( (TAnd( lt rt )) (
         (set tt (TAnd(
            (close(substitute( tctx lt )))
            (close(substitute( tctx rt )))
         )))
      ))
      ( _ () )
   ))
   tt
) Type);

substitute-lhs := λ(: tctx TContext)(: t AST). (: (
   (match t (
      ()
      ( (App( ps (App( (Lit( ':_s ctk )) (App( (Var( v vtk )) (AType vt) )) )) )) (
         (set t (App(
            (close(substitute-lhs( tctx ps )))
            (close(App( (close(Lit( ':_s (unique ctk) ))) (close(App(
               (close(Var( v (unique vtk) )))
               (close(AType( (substitute( tctx vt )) )))
            ))) )))
         )))
      ))
      ( (App( (Lit( ':_s ctk )) (App( (Var( v vtk )) (AType vt) )) )) (
         (set t (App( (close(Lit( ':_s (unique ctk) ))) (close(App(
            (close(Var( v (unique vtk) )))
            (close(AType( (substitute( tctx vt )) )))
         ))) )))
      ))
      ( (App( ps (Var( v vtk )) )) (
         (set t (App(
            (close(substitute-lhs( tctx ps )))
            (close(Var( v (unique vtk) )))
         )))
      ))
      ( (Var( v vtk )) (set t (Var( v (unique vtk) ))) )
      ( ASTNil () )
      ( _ (exit-error( 'Unexpected\sSubstitute\sLHS_s t )) )
   ))
   t
) AST);

substitute := λ(: tctx TContext)(: t AST). (: (
   (match t (
      ()
      ( ASTEOF () )
      ( ASTNil () )
      ( (App( (Lit( ':_s ctk )) (App( (Lit( v vtk )) (AType vt) )) )) (
         (set t (App( (close(Lit( ':_s (unique ctk) ))) (close(App(
            (close(Lit( v (unique vtk) )))
            (close(AType( (substitute( tctx vt )) )))
         ))) )))
         (while (non-zero tctx) (match tctx (
            ()
            ( TCtxNil (set tctx TCtxEOF) )
            ( (TCtxBind( rst tk tv ta )) (
               (if (==( tk v )) (
                  (set t (App( (close(Lit( ':_s (unique ctk) ))) (close(App(
                     (close(substitute( tctx ta )))
                     (close(AType( (substitute( tctx vt )) )))
                  ))) )))
                  (set tctx TCtxEOF)
               ) (set tctx rst))
            ))
         )))
      ))
      ( (App( (Lit( ':_s ctk )) (App( (Var( v vtk )) (AType vt) )) )) (
         (set t (App( (close(Lit( ':_s (unique ctk) ))) (close(App(
            (close(Var( v (unique vtk) )))
            (close(AType( (substitute( tctx vt )) )))
         ))) )))
         (while (non-zero tctx) (match tctx (
            ()
            ( TCtxNil (set tctx TCtxEOF) )
            ( (TCtxBind( rst tk tv ta )) (
               (if (==( tk v )) (
                  (set t (App( (close(Lit( ':_s (unique ctk) ))) (close(App(
                     (close(substitute( tctx ta )))
                     (close(AType( (substitute( tctx vt )) )))
                  ))) )))
                  (set tctx TCtxEOF)
               ) (set tctx rst))
            ))
         )))
      ))
      ( (Lit( v vtk )) (set t (Lit( v (unique vtk) ))) )
      ( (Var( v vtk )) (set t (Var( v (unique vtk) ))) )
      ( (Abs( lhs rhs tt )) (
         (set t (Abs(
            (close(substitute-lhs( tctx lhs )))
            (close(substitute( tctx rhs )))
            (substitute( tctx tt ))
         )))
      ))
      ( (AType( tt )) (
         (set t (AType( (substitute( tctx tt )) )))
      ))
      ( (App( lt rt )) (
         (set t (App(
            (close(substitute( tctx lt )))
            (close(substitute( tctx rt )))
         )))
      ))
      ( (Seq( lt rt )) (
         (set t (Seq(
            (close(substitute( tctx lt )))
            (close(substitute( tctx rt )))
         )))
      ))
      ( (Glb( k rt )) (
         (set t (Glb(
            (unique k)
            (close(substitute( tctx rt )))
         )))
      ))
      ( (Typedef( lt rt )) (
         (set t (Typedef(
            (close(substitute( tctx lt )))
            (close(substitute( tctx rt )))
         )))
      ))
      ( (Frg( k lt )) (
         (set t (Frg(
            (unique k)
            (close(substitute( tctx lt )))
         )))
      ))
      ( _ (exit-error( 'Unexpected\sSubstitution\sTerm:_s t )) )
   ))
   t
) AST);

substitute := λ(: tctx StringSList)(: t S). (: (
   (match t (
      ()
      ( SNil (set t SNil) )
      ( (SAtom a) (
         (while (non-zero tctx) (match tctx (
            ()
            ( (SSLSeq( rst k v )) (
               (if (==( a k )) (
                  (set t v)
               ) ())
               (set tctx rst)
            )))
         ))
      ))
      ( (SCons( lt rt )) (
         (set t (SCons(
            (close(substitute( tctx lt )))
            (close(substitute( tctx rt )))
         )))
      ))
   ))
   (let rt t)
   rt
) S);