-fact at_inv_cons_aux: â\88\80cs,i1,i2. @â¦\83i1, csâ¦\84 ≘ i2 →
- ∀l,m,cs0. cs = {l, m};cs0 →
- i1 < l â\88§ @â¦\83i1, cs0â¦\84 ≘ i2 ∨
- l â\89¤ i1 â\88§ @â¦\83i1 + m, cs0â¦\84 ≘ i2.
+fact at_inv_cons_aux: â\88\80cs,i1,i2. @â\9dªi1, csâ\9d« ≘ i2 →
+ ∀l,m,cs0. cs = ❨l, m❩;cs0 →
+ i1 < l â\88§ @â\9dªi1, cs0â\9d« ≘ i2 ∨
+ l â\89¤ i1 â\88§ @â\9dªi1 + m, cs0â\9d« ≘ i2.