-lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≘ i2 → @⦃↑i1, n@f⦄ ≘ ↑(n+i2).
+lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≘ i2 → @⦃↑i1, n⨮f⦄ ≘ ↑(n+i2).
-lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≘ i → @⦃i1, (m+n)@f⦄ ≘ m+i.
+lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n⨮f⦄ ≘ i → @⦃i1, (m+n)⨮f⦄ ≘ m+i.
#f #i1 #i #n #m #H elim m -m //
#m <plus_S1 /2 width=5 by at_next/ (**) (* full auto fails *)
qed.
(* Specific inversion lemmas on at ******************************************)
#f #i1 #i #n #m #H elim m -m //
#m <plus_S1 /2 width=5 by at_next/ (**) (* full auto fails *)
qed.
(* Specific inversion lemmas on at ******************************************)
-lemma at_inv_O1: ∀f,n,i2. @⦃0, n@f⦄ ≘ i2 → n = i2.
+lemma at_inv_O1: ∀f,n,i2. @⦃0, n⨮f⦄ ≘ i2 → n = i2.
#f #n elim n -n /2 width=6 by at_inv_ppx/
#n #IH #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
#j2 #Hj * -i2 /3 width=1 by eq_f/
qed-.
#f #n elim n -n /2 width=6 by at_inv_ppx/
#n #IH #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
#j2 #Hj * -i2 /3 width=1 by eq_f/
qed-.
-lemma at_inv_S1: ∀f,n,j1,i2. @⦃↑j1, n@f⦄ ≘ i2 →
+lemma at_inv_S1: ∀f,n,j1,i2. @⦃↑j1, n⨮f⦄ ≘ i2 →
∃∃j2. @⦃j1, f⦄ ≘ j2 & ↑(n+j2) = i2.
#f #n elim n -n /2 width=5 by at_inv_npx/
#n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
∃∃j2. @⦃j1, f⦄ ≘ j2 & ↑(n+j2) = i2.
#f #n elim n -n /2 width=5 by at_inv_npx/
#n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
-lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n@f⦄ ≘ i2 → i1 + n ≤ i2.
+lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n⨮f⦄ ≘ i2 → i1 + n ≤ i2.
-lemma at_fwd_id: ∀f,n,i. @⦃i, n@f⦄ ≘ i → 0 = n.
+lemma at_fwd_id: ∀f,n,i. @⦃i, n⨮f⦄ ≘ i → 0 = n.