-fact at_inv_cons_aux: ∀des,i1,i2. @[i1] des ≡ i2 →
- ∀d,e,des0. des = {d, e} :: des0 →
- i1 < d ∧ @[i1] des0 ≡ i2 ∨
- d ≤ i1 ∧ @[i1 + e] des0 ≡ i2.
+fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 →
+ ∀d,e,des0. des = {d, e} @ des0 →
+ i1 < d ∧ @⦃i1, des0⦄ ≡ i2 ∨
+ d ≤ i1 ∧ @⦃i1 + e, des0⦄ ≡ i2.