-fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 →
- ∀l,m,des0. des = {l, m} @ des0 →
- i1 < l ∧ @⦃i1, des0⦄ ≡ i2 ∨
- l ≤ i1 ∧ @⦃i1 + m, des0⦄ ≡ i2.
-#des #i1 #i2 * -des -i1 -i2
-[ #i #l #m #des #H destruct
-| #des1 #l1 #m1 #i1 #i2 #Hil1 #Hi12 #l2 #m2 #des2 #H destruct /3 width=1 by or_introl, conj/
-| #des1 #l1 #m1 #i1 #i2 #Hli1 #Hi12 #l2 #m2 #des2 #H destruct /3 width=1 by or_intror, conj/
+fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 →
+ ∀l,m,cs0. cs = {l, m} @ cs0 →
+ i1 < l ∧ @⦃i1, cs0⦄ ≡ i2 ∨
+ l ≤ i1 ∧ @⦃i1 + m, cs0⦄ ≡ i2.
+#cs #i1 #i2 * -cs -i1 -i2
+[ #i #l #m #cs #H destruct
+| #cs1 #l1 #m1 #i1 #i2 #Hil1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/
+| #cs1 #l1 #m1 #i1 #i2 #Hli1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_intror, conj/