DEFINITION subst0_tlt()
TYPE =
       ∀u:T.∀t:T.∀z:T.(subst0 O u t z)→(tlt z (THead (Bind Abbr) u t))
BODY =
Show proof