#x2 #Hg * -i2 #H destruct //
qed-.
-(* --------------------------------------------------------------------------*)
-
lemma at_inv_pxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → 0 = i1 → 0 = i2 → ∃g. ↑g = f.
#f elim (pn_split … f) * /2 width=2 by ex_intro/
#g #H #i1 #i2 #Hf #H1 #H2 cases (at_inv_xnp … Hf … H H2)
/4 width=7 by at_inv_xnn, at_inv_npn, ex2_intro, or_intror, or_introl/
qed-.
-(* --------------------------------------------------------------------------*)
-
+(* Note: the following inversion lemmas must be checked *)
lemma at_inv_xpx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ↑g = f →
(0 = i1 ∧ 0 = i2) ∨
∃∃j1,j2. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1 & ⫯j2 = i2.
(* Basic properties *********************************************************)
-let corec at_eq_repl_back: ∀i1,i2. eq_repl_back (λf. @⦃i1, f⦄ ≡ i2) ≝ ?.
+corec lemma at_eq_repl_back: ∀i1,i2. eq_repl_back (λf. @⦃i1, f⦄ ≡ i2).
#i1 #i2 #f1 #H1 cases H1 -f1 -i1 -i2
[ #f1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /2 width=2 by at_refl/
| #f1 #i1 #i2 #Hf1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /3 width=7 by at_push/
#Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/
qed-.
-(* Properties on minus ******************************************************)
+(* Properties on tls ********************************************************)
-lemma at_pxx_minus: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, f-n⦄ ≡ 0.
+lemma at_pxx_tls: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, ⫱*[n]f⦄ ≡ 0.
#n elim n -n //
#n #IH #f #Hf cases (at_inv_pxn … Hf) -Hf /2 width=3 by/
qed.
+lemma at_tls: ∀i2,f. ↑⫱*[⫯i2]f ≗ ⫱*[i2]f → ∃i1. @⦃i1, f⦄ ≡ i2.
+#i2 elim i2 -i2
+[ /4 width=4 by at_eq_repl_back, at_refl, ex_intro/
+| #i2 #IH #f <tls_xn <tls_xn in ⊢ (??%→?); #H
+ elim (IH … H) -IH -H #i1 #Hf
+ elim (pn_split f) * #g #Hg destruct /3 width=8 by at_push, at_next, ex_intro/
+]
+qed-.
+
+(* Inversion lemmas with tls ************************************************)
+
+lemma at_inv_tls: ∀i2,i1,f. @⦃i1, f⦄ ≡ i2 → ↑⫱*[⫯i2]f ≗ ⫱*[i2]f.
+#i2 elim i2 -i2
+[ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf // #g #H1 #H destruct
+ /2 width=1 by eq_refl/
+| #i2 #IH #i1 #f #Hf elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ] /2 width=2 by/
+]
+qed-.
+
(* Advanced inversion lemmas on isid ****************************************)
lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i.
lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈⦃f⦄ → @⦃i1, f⦄ ≡ i2 → i1 = i2.
/3 width=6 by isid_inv_at, at_mono/ qed-.
-(* Advancedd properties on isid *********************************************)
+(* Advanced properties on isid **********************************************)
-let corec isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄ ≝ ?.
+corec lemma isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄.
#f #Hf lapply (Hf 0)
#H cases (at_fwd_id_ex … H) -H
#g #H @(isid_push … H) /3 width=7 by at_inv_npn/