i) O x))).(let H_x0 \def (lift_gen_lref x O (S i) j H3) in (let H4 \def H_x0
in (or_ind (land (lt j O) (eq T x (TLRef j))) (land (le (plus O (S i)) j) (eq
T x (TLRef (minus j (S i))))) (lt i j) (\lambda (H5: (land (lt j O) (eq T x
i) O x))).(let H_x0 \def (lift_gen_lref x O (S i) j H3) in (let H4 \def H_x0
in (or_ind (land (lt j O) (eq T x (TLRef j))) (land (le (plus O (S i)) j) (eq
T x (TLRef (minus j (S i))))) (lt i j) (\lambda (H5: (land (lt j O) (eq T x