infer-ctx := λ(: tctx TContext)(: lhs AST). (: (
   (match lhs (
      ()
      ( (App( (Lit( ':_s _ )) (App( (Var( v vtk )) (AType tt) )) )) (
         (set tt (denormalize tt))
         (set tctx (TCtxBind(
            (close tctx) v (as-local-variable tt) (Var( v vtk ))
         )))
         (set tctx (infer-tctx( tctx tt )))
      ))
      ( (App( ps (App( (Lit( ':_s _ )) (App( (Var( v vtk )) (AType tt) )) )) )) (
         (set tt (denormalize tt))
         (set tctx (TCtxBind(
            (close tctx) v (as-local-variable tt) (Var( v vtk ))
         )))
         (set tctx (infer-ctx( tctx ps )))
         (set tctx (infer-tctx( tctx tt )))
      ))
      ( ASTNil () )
      ( _ (exit-error( 'Invalid\sLHS_s lhs )) )
   ))
   tctx
) TContext);