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