-lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} @ des2 →
- ∃∃des1. des1 + i = des2 & des = {d - i, e} @ des1.
-#i #d #e #des2 * normalize
+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