- | tlref_map_lref_lt: \forall j. \forall i. \forall y. (lt j i) \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y j))
- | tlref_map_lref_ge: \forall j. \forall i. \forall y. (le i j) \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y (map j))).
\ No newline at end of file
+ | tlref_map_lref_lt: \forall j. \forall i. \forall y. j < i \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y j))
+ | tlref_map_lref_ge: \forall j. \forall i. \forall y. i \le j \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y (map j))).