-(H5: (land (le (plus O (S i)) j) (eq T x (TLRef (minus j (S i)))))).(land_ind
-(le (plus O (S i)) j) (eq T x (TLRef (minus j (S i)))) (lt i j) (\lambda (H6:
-(le (plus O (S i)) j)).(\lambda (_: (eq T x (TLRef (minus j (S i))))).H6))
-H5)) H4))))) H2))))))))).
+(H5: (land (le (S i) j) (eq T x (TLRef (minus j (S i)))))).(land_ind (le (S
+i) j) (eq T x (TLRef (minus j (S i)))) (lt i j) (\lambda (H6: (le (S i)
+j)).(\lambda (_: (eq T x (TLRef (minus j (S i))))).H6)) H5)) H4)))))
+H2))))))))).