assert-well-typed := λ(: term AST). (: (
   (match term (
      ()
      ( ASTEOF (assert-one-typed term) )
      ( ASTNil (assert-one-typed term) )
      ( (Glb( k v )) (
         (if (is-open(typeof term)) () (
            (assert-well-typed v)
         ))
      ))
      ( (Frg( _ v )) (
         (assert-one-typed v)
      ))
      ( (Typedef( _ _ )) () )
      ( (App( (Abs( (Var( lname _ )) ASTNil tlt )) rhs )) (
         (assert-well-typed rhs)
         (assert-one-typed term)
      ))
      ( (App( (Var( 'gensym-label_s _ )) _ )) () )
      ( (App( (Var( 'label_s _ )) (Var( _ _ )) )) () )
      ( (App( (App( (Var( 'while_s _ )) cond )) body )) (
         (assert-well-typed cond)
         (assert-well-typed body)
         (assert-one-typed term)
      ))
      ( (App( (Var( 'as_s _ )) (App( t (AType tt) )) )) (
         (assert-well-typed t)
      ))
      ( (App( (Lit( ':_s _ )) (App( t (AType tt) )) )) (
         (assert-well-typed t)
      ))
      ( (App( (App( (App( (Var( 'if_s _ )) cond )) t )) f )) (
         (assert-well-typed cond)
         (assert-well-typed t)
         (assert-well-typed f)
         (assert-one-typed term)
      ))
      ( (App( (App( (Var( 'set_s _ )) lhs )) rhs )) (
         (assert-well-typed rhs)
         (assert-one-typed term)
      ))
      ( (AType _) () )
      ( (App( (Var( 'open_s _ )) rterm )) (
         (assert-well-typed rterm)
         (assert-one-typed term)
      ))
      ( (App( (Var( 'scope_s _ )) rterm )) (
         (assert-well-typed rterm)
         (assert-one-typed term)
      ))
      ( (Lit( l _ )) (assert-one-typed term) )
      ( (Var( l _ )) (assert-one-typed term) )
      ( (Abs( lhs rhs tlt )) (
         (assert-well-typed rhs)
         (assert-one-typed term)
      ))
      ( (App( l r )) (
         (assert-well-typed l)
         (assert-well-typed r)
         (assert-one-typed term)
      ))
      ( (Seq( l r )) (
         (assert-well-typed l)
         (assert-well-typed r)
      ))
      ( (Meta( _ )) () )
      ( _ (
         (print 'Unknown\sTerm\sIn\sAssert\sWell\sTyped\s_s)(print term)(print '\n_s)
         (exit 1_u64)
      ))
   ))
) Nil);