-lemma at_inv_tls: ∀i2,i1,f. @⦃i1, f⦄ ≡ i2 → ↑⫱*[⫯i2]f ≗ ⫱*[i2]f.
+lemma at_inv_nxx: ∀n,g,i1,j2. @⦃↑i1,g⦄ ≘ j2 → @⦃0,g⦄ ≘ n →
+ ∃∃i2. @⦃i1,⫱*[↑n]g⦄ ≘ i2 & ↑(n+i2) = j2.
+#n elim n -n
+[ #g #i1 #j2 #Hg #H
+ elim (at_inv_pxp … H) -H [ |*: // ] #f #H0
+ elim (at_inv_npx … Hg … H0) -Hg [ |*: // ] #x2 #Hf #H2 destruct
+ /2 width=3 by ex2_intro/
+| #n #IH #g #i1 #j2 #Hg #H
+ elim (at_inv_pxn … H) -H [ |*: // ] #f #Hf2 #H0
+ elim (at_inv_xnx … Hg … H0) -Hg #x2 #Hf1 #H2 destruct
+ elim (IH … Hf1 Hf2) -IH -Hf1 -Hf2 #i2 #Hf #H2 destruct
+ /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma at_inv_tls: ∀i2,i1,f. @⦃i1,f⦄ ≘ i2 → ⫯⫱*[↑i2]f ≡ ⫱*[i2]f.