as-local-variable := λ(: tt Type). (: (
   (set tt (normalize tt))
   (if (non-zero tt) (
      (set tt (TAnd( (close tt) (close(t1 'LocalVariable_s)) )))
   ) ())
   (set tt (with-size tt))
   tt
) Type);