DEFINITION subst0_tlt()
TYPE =
       ∀u:T.∀t:T.∀z:T.(subst0 O u t z)→(tlt z (THead (Bind Abbr) u t))
BODY =
        assume u: T
        assume t: T
        assume z: T
        suppose H: subst0 O u t z
          (h1) 
             by (tlt_head_dx . . .)
tlt z (THead (Bind Abbr) u z)
          end of h1
          (h2) 
             by (subst0_tlt_head . . . H)
tlt (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)
          end of h2
          by (tlt_trans . . . h1 h2)
          we proved tlt z (THead (Bind Abbr) u t)
       we proved ∀u:T.∀t:T.∀z:T.(subst0 O u t z)→(tlt z (THead (Bind Abbr) u t))