-| at_lt : ∀des,d,e,i1,i2. i1 < d →
- at des i1 i2 → at ({d, e} @ des) i1 i2
-| at_ge : ∀des,d,e,i1,i2. d ≤ i1 →
- at des (i1 + e) i2 → at ({d, e} @ des) i1 i2
+| at_lt : ∀des,l,m,i1,i2. i1 < l →
+ at des i1 i2 → at ({l, m} @ des) i1 i2
+| at_ge : ∀des,l,m,i1,i2. l ≤ i1 →
+ at des (i1 + m) i2 → at ({l, m} @ des) i1 i2