\forall (v: T).(\forall (i: nat).(eq T (subst i v (TLRef i)) (lift i O v)))
\def
\lambda (v: T).(\lambda (i: nat).(eq_ind_r bool false (\lambda (b: bool).(eq
\forall (v: T).(\forall (i: nat).(eq T (subst i v (TLRef i)) (lift i O v)))
\def
\lambda (v: T).(\lambda (i: nat).(eq_ind_r bool false (\lambda (b: bool).(eq