-lemma pluss_inv_cons2: ∀i,l,m,des2,des. des + i = {l, m} @ des2 →
- ∃∃des1. des1 + i = des2 & des = {l - i, m} @ des1.
-#i #l #m #des2 * normalize
+lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} @ cs2 →
+ ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} @ cs1.
+#i #l #m #cs2 * normalize