(eq T t (TLRef n)) (land (eq nat n i) (eq T t (lift (S n) O v))))) (or_introl
(eq T (TLRef n) (TLRef n)) (land (eq nat n i) (eq T (TLRef n) (lift (S n) O
v))) (refl_equal T (TLRef n))) (\lambda (t2: T).(\lambda (H0: (subst0 i v
(eq T t (TLRef n)) (land (eq nat n i) (eq T t (lift (S n) O v))))) (or_introl
(eq T (TLRef n) (TLRef n)) (land (eq nat n i) (eq T (TLRef n) (lift (S n) O
v))) (refl_equal T (TLRef n))) (\lambda (t2: T).(\lambda (H0: (subst0 i v