'RAt i1 f i2 = (at f i1 i2).
definition H_at_div: relation4 rtmap rtmap rtmap rtmap ≝ λf2,g2,f1,g1.
- â\88\80jf,jg,j. @â¦\83jf,f2â¦\84 â\89\98 j â\86\92 @â¦\83jg,g2â¦\84 ≘ j →
- â\88\83â\88\83j0. @â¦\83j0,f1â¦\84 â\89\98 jf & @â¦\83j0,g1â¦\84 ≘ jg.
+ â\88\80jf,jg,j. @â\9dªjf,f2â\9d« â\89\98 j â\86\92 @â\9dªjg,g2â\9d« ≘ j →
+ â\88\83â\88\83j0. @â\9dªj0,f1â\9d« â\89\98 jf & @â\9dªj0,g1â\9d« ≘ jg.
(* Basic inversion lemmas ***************************************************)
-lemma at_inv_ppx: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 → ∀g. 0 = i1 → ⫯g = f → 0 = i2.
+lemma at_inv_ppx: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 → ∀g. 0 = i1 → ⫯g = f → 0 = i2.
#f #i1 #i2 * -f -i1 -i2 //
[ #f #i1 #i2 #_ #g #j1 #j2 #_ * #_ #x #H destruct
| #f #i1 #i2 #_ #g #j2 * #_ #x #_ #H elim (discr_push_next … H)
]
qed-.
-lemma at_inv_npx: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
- â\88\83â\88\83j2. @â¦\83j1,gâ¦\84 ≘ j2 & ↑j2 = i2.
+lemma at_inv_npx: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
+ â\88\83â\88\83j2. @â\9dªj1,gâ\9d« ≘ j2 & ↑j2 = i2.
#f #i1 #i2 * -f -i1 -i2
[ #f #g #j1 #j2 #_ * #_ #x #x1 #H destruct
| #f #i1 #i2 #Hi #g #j1 #j2 * * * #x #x1 #H #Hf >(injective_push … Hf) -g destruct /2 width=3 by ex2_intro/
]
qed-.
-lemma at_inv_xnx: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 → ∀g. ↑g = f →
- â\88\83â\88\83j2. @â¦\83i1,gâ¦\84 ≘ j2 & ↑j2 = i2.
+lemma at_inv_xnx: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 → ∀g. ↑g = f →
+ â\88\83â\88\83j2. @â\9dªi1,gâ\9d« ≘ j2 & ↑j2 = i2.
#f #i1 #i2 * -f -i1 -i2
[ #f #g #j1 #j2 * #_ #_ #x #H elim (discr_next_push … H)
| #f #i1 #i2 #_ #g #j1 #j2 * #_ #_ #x #H elim (discr_next_push … H)
(* Advanced inversion lemmas ************************************************)
-lemma at_inv_ppn: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 →
+lemma at_inv_ppn: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 →
∀g,j2. 0 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
#f #i1 #i2 #Hf #g #j2 #H1 #H <(at_inv_ppx … Hf … H1 H) -f -g -i1 -i2
#H destruct
qed-.
-lemma at_inv_npp: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 →
+lemma at_inv_npp: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 →
∀g,j1. ↑j1 = i1 → ⫯g = f → 0 = i2 → ⊥.
#f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
#x2 #Hg * -i2 #H destruct
qed-.
-lemma at_inv_npn: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 →
- â\88\80g,j1,j2. â\86\91j1 = i1 â\86\92 ⫯g = f â\86\92 â\86\91j2 = i2 â\86\92 @â¦\83j1,gâ¦\84 ≘ j2.
+lemma at_inv_npn: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 →
+ â\88\80g,j1,j2. â\86\91j1 = i1 â\86\92 ⫯g = f â\86\92 â\86\91j2 = i2 â\86\92 @â\9dªj1,gâ\9d« ≘ j2.
#f #i1 #i2 #Hf #g #j1 #j2 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
#x2 #Hg * -i2 #H destruct //
qed-.
-lemma at_inv_xnp: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 →
+lemma at_inv_xnp: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 →
∀g. ↑g = f → 0 = i2 → ⊥.
#f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f
#x2 #Hg * -i2 #H destruct
qed-.
-lemma at_inv_xnn: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 →
- â\88\80g,j2. â\86\91g = f â\86\92 â\86\91j2 = i2 â\86\92 @â¦\83i1,gâ¦\84 ≘ j2.
+lemma at_inv_xnn: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 →
+ â\88\80g,j2. â\86\91g = f â\86\92 â\86\91j2 = i2 â\86\92 @â\9dªi1,gâ\9d« ≘ j2.
#f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xnx … Hf … H) -f
#x2 #Hg * -i2 #H destruct //
qed-.
-lemma at_inv_pxp: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 → 0 = i1 → 0 = i2 → ∃g. ⫯g = f.
+lemma at_inv_pxp: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ 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)
qed-.
-lemma at_inv_pxn: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 → ∀j2. 0 = i1 → ↑j2 = i2 →
- â\88\83â\88\83g. @â¦\83i1,gâ¦\84 ≘ j2 & ↑g = f.
+lemma at_inv_pxn: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 → ∀j2. 0 = i1 → ↑j2 = i2 →
+ â\88\83â\88\83g. @â\9dªi1,gâ\9d« ≘ j2 & ↑g = f.
#f elim (pn_split … f) *
#g #H #i1 #i2 #Hf #j2 #H1 #H2
[ elim (at_inv_ppn … Hf … H1 H H2)
]
qed-.
-lemma at_inv_nxp: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 →
+lemma at_inv_nxp: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 →
∀j1. ↑j1 = i1 → 0 = i2 → ⊥.
#f elim (pn_split f) *
#g #H #i1 #i2 #Hf #j1 #H1 #H2
]
qed-.
-lemma at_inv_nxn: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
- (â\88\83â\88\83g. @â¦\83j1,gâ¦\84 ≘ j2 & ⫯g = f) ∨
- â\88\83â\88\83g. @â¦\83i1,gâ¦\84 ≘ j2 & ↑g = f.
+lemma at_inv_nxn: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
+ (â\88\83â\88\83g. @â\9dªj1,gâ\9d« ≘ j2 & ⫯g = f) ∨
+ â\88\83â\88\83g. @â\9dªi1,gâ\9d« ≘ j2 & ↑g = f.
#f elim (pn_split f) *
/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: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 → ∀g. ⫯g = f →
+lemma at_inv_xpx: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 → ∀g. ⫯g = f →
(0 = i1 ∧ 0 = i2) ∨
- â\88\83â\88\83j1,j2. @â¦\83j1,gâ¦\84 ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
+ â\88\83â\88\83j1,j2. @â\9dªj1,gâ\9d« ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
#f * [2: #i1 ] #i2 #Hf #g #H
[ elim (at_inv_npx … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
| >(at_inv_ppx … Hf … H) -f /3 width=1 by conj, or_introl/
]
qed-.
-lemma at_inv_xpp: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 → ∀g. ⫯g = f → 0 = i2 → 0 = i1.
+lemma at_inv_xpp: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 → ∀g. ⫯g = f → 0 = i2 → 0 = i1.
#f #i1 #i2 #Hf #g #H elim (at_inv_xpx … Hf … H) -f * //
#j1 #j2 #_ #_ * -i2 #H destruct
qed-.
-lemma at_inv_xpn: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
- â\88\83â\88\83j1. @â¦\83j1,gâ¦\84 ≘ j2 & ↑j1 = i1.
+lemma at_inv_xpn: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
+ â\88\83â\88\83j1. @â\9dªj1,gâ\9d« ≘ j2 & ↑j1 = i1.
#f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xpx … Hf … H) -f *
[ #_ * -i2 #H destruct
| #x1 #x2 #Hg #H1 * -i2 #H destruct /2 width=3 by ex2_intro/
]
qed-.
-lemma at_inv_xxp: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 → 0 = i2 →
+lemma at_inv_xxp: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 → 0 = i2 →
∃∃g. 0 = i1 & ⫯g = f.
#f elim (pn_split f) *
#g #H #i1 #i2 #Hf #H2
]
qed-.
-lemma at_inv_xxn: â\88\80f,i1,i2. @â¦\83i1,fâ¦\84 ≘ i2 → ∀j2. ↑j2 = i2 →
- (â\88\83â\88\83g,j1. @â¦\83j1,gâ¦\84 ≘ j2 & ↑j1 = i1 & ⫯g = f) ∨
- â\88\83â\88\83g. @â¦\83i1,gâ¦\84 ≘ j2 & ↑g = f.
+lemma at_inv_xxn: â\88\80f,i1,i2. @â\9dªi1,fâ\9d« ≘ i2 → ∀j2. ↑j2 = i2 →
+ (â\88\83â\88\83g,j1. @â\9dªj1,gâ\9d« ≘ j2 & ↑j1 = i1 & ⫯g = f) ∨
+ â\88\83â\88\83g. @â\9dªi1,gâ\9d« ≘ j2 & ↑g = f.
#f elim (pn_split f) *
#g #H #i1 #i2 #Hf #j2 #H2
[ elim (at_inv_xpn … Hf … H H2) -i2 /3 width=5 by or_introl, ex3_2_intro/
(* Basic forward lemmas *****************************************************)
-lemma at_increasing: â\88\80i2,i1,f. @â¦\83i1,fâ¦\84 ≘ i2 → i1 ≤ i2.
+lemma at_increasing: â\88\80i2,i1,f. @â\9dªi1,fâ\9d« ≘ i2 → i1 ≤ i2.
#i2 elim i2 -i2
[ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf //
| #i2 #IH * //
]
qed-.
-lemma at_increasing_strict: â\88\80g,i1,i2. @â¦\83i1,gâ¦\84 ≘ i2 → ∀f. ↑f = g →
- i1 < i2 â\88§ @â¦\83i1,fâ¦\84 ≘ ↓i2.
+lemma at_increasing_strict: â\88\80g,i1,i2. @â\9dªi1,gâ\9d« ≘ i2 → ∀f. ↑f = g →
+ i1 < i2 â\88§ @â\9dªi1,fâ\9d« ≘ ↓i2.
#g #i1 #i2 #Hg #f #H elim (at_inv_xnx … Hg … H) -Hg -H
/4 width=2 by conj, at_increasing, le_S_S/
qed-.
-lemma at_fwd_id_ex: â\88\80f,i. @â¦\83i,fâ¦\84 ≘ i → ∃g. ⫯g = f.
+lemma at_fwd_id_ex: â\88\80f,i. @â\9dªi,fâ\9d« ≘ i → ∃g. ⫯g = f.
#f elim (pn_split f) * /2 width=2 by ex_intro/
#g #H #i #Hf elim (at_inv_xnx … Hf … H) -Hf -H
#j2 #Hg #H destruct lapply (at_increasing … Hg) -Hg
(* Basic properties *********************************************************)
-corec lemma at_eq_repl_back: â\88\80i1,i2. eq_repl_back (λf. @â¦\83i1,fâ¦\84 ≘ i2).
+corec lemma at_eq_repl_back: â\88\80i1,i2. eq_repl_back (λf. @â\9dªi1,fâ\9d« ≘ 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/
]
qed-.
-lemma at_eq_repl_fwd: â\88\80i1,i2. eq_repl_fwd (λf. @â¦\83i1,fâ¦\84 ≘ i2).
+lemma at_eq_repl_fwd: â\88\80i1,i2. eq_repl_fwd (λf. @â\9dªi1,fâ\9d« ≘ i2).
#i1 #i2 @eq_repl_sym /2 width=3 by at_eq_repl_back/
qed-.
-lemma at_le_ex: â\88\80j2,i2,f. @â¦\83i2,fâ¦\84 ≘ j2 → ∀i1. i1 ≤ i2 →
- â\88\83â\88\83j1. @â¦\83i1,fâ¦\84 ≘ j1 & j1 ≤ j2.
+lemma at_le_ex: â\88\80j2,i2,f. @â\9dªi2,fâ\9d« ≘ j2 → ∀i1. i1 ≤ i2 →
+ â\88\83â\88\83j1. @â\9dªi1,fâ\9d« ≘ j1 & j1 ≤ j2.
#j2 elim j2 -j2 [2: #j2 #IH ] #i2 #f #Hf
[ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
#g [ #x2 ] #Hg [ #H2 ] #H0
]
qed-.
-lemma at_id_le: â\88\80i1,i2. i1 â\89¤ i2 â\86\92 â\88\80f. @â¦\83i2,fâ¦\84 â\89\98 i2 â\86\92 @â¦\83i1,fâ¦\84 ≘ i1.
+lemma at_id_le: â\88\80i1,i2. i1 â\89¤ i2 â\86\92 â\88\80f. @â\9dªi2,fâ\9d« â\89\98 i2 â\86\92 @â\9dªi1,fâ\9d« ≘ i1.
#i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ]
#f #Hf elim (at_fwd_id_ex … Hf) /4 width=7 by at_inv_npn, at_push, at_refl/
qed-.
(* Main properties **********************************************************)
-theorem at_monotonic: â\88\80j2,i2,f. @â¦\83i2,fâ¦\84 â\89\98 j2 â\86\92 â\88\80j1,i1. @â¦\83i1,fâ¦\84 ≘ j1 →
+theorem at_monotonic: â\88\80j2,i2,f. @â\9dªi2,fâ\9d« â\89\98 j2 â\86\92 â\88\80j1,i1. @â\9dªi1,fâ\9d« ≘ j1 →
i1 < i2 → j1 < j2.
#j2 elim j2 -j2
[ #i2 #f #H2f elim (at_inv_xxp … H2f) -H2f //
]
qed-.
-theorem at_inv_monotonic: â\88\80j1,i1,f. @â¦\83i1,fâ¦\84 â\89\98 j1 â\86\92 â\88\80j2,i2. @â¦\83i2,fâ¦\84 ≘ j2 →
+theorem at_inv_monotonic: â\88\80j1,i1,f. @â\9dªi1,fâ\9d« â\89\98 j1 â\86\92 â\88\80j2,i2. @â\9dªi2,fâ\9d« ≘ j2 →
j1 < j2 → i1 < i2.
#j1 elim j1 -j1
[ #i1 #f #H1f elim (at_inv_xxp … H1f) -H1f //
]
qed-.
-theorem at_mono: â\88\80f,i,i1. @â¦\83i,fâ¦\84 â\89\98 i1 â\86\92 â\88\80i2. @â¦\83i,fâ¦\84 ≘ i2 → i2 = i1.
+theorem at_mono: â\88\80f,i,i1. @â\9dªi,fâ\9d« â\89\98 i1 â\86\92 â\88\80i2. @â\9dªi,fâ\9d« ≘ i2 → i2 = i1.
#f #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
#Hi elim (lt_le_false i i) /3 width=6 by at_inv_monotonic, eq_sym/
qed-.
-theorem at_inj: â\88\80f,i1,i. @â¦\83i1,fâ¦\84 â\89\98 i â\86\92 â\88\80i2. @â¦\83i2,fâ¦\84 ≘ i → i1 = i2.
+theorem at_inj: â\88\80f,i1,i. @â\9dªi1,fâ\9d« â\89\98 i â\86\92 â\88\80i2. @â\9dªi2,fâ\9d« ≘ i → i1 = i2.
#f #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
#Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/
qed-.
(* Properties on tls ********************************************************)
-lemma at_pxx_tls: â\88\80n,f. @â¦\830,fâ¦\84 â\89\98 n â\86\92 @â¦\830,⫱*[n]fâ¦\84 ≘ 0.
+lemma at_pxx_tls: â\88\80n,f. @â\9dª0,fâ\9d« â\89\98 n â\86\92 @â\9dª0,⫱*[n]fâ\9d« ≘ 0.
#n elim n -n //
#n #IH #f #Hf
cases (at_inv_pxn … Hf) -Hf [ |*: // ] #g #Hg #H0 destruct
<tls_xn /2 width=1 by/
qed.
-lemma at_tls: â\88\80i2,f. ⫯⫱*[â\86\91i2]f â\89¡ ⫱*[i2]f â\86\92 â\88\83i1. @â¦\83i1,fâ¦\84 ≘ i2.
+lemma at_tls: â\88\80i2,f. ⫯⫱*[â\86\91i2]f â\89¡ ⫱*[i2]f â\86\92 â\88\83i1. @â\9dªi1,fâ\9d« ≘ 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
(* Inversion lemmas with tls ************************************************)
-lemma at_inv_nxx: â\88\80n,g,i1,j2. @â¦\83â\86\91i1,gâ¦\84 â\89\98 j2 â\86\92 @â¦\830,gâ¦\84 ≘ n →
- â\88\83â\88\83i2. @â¦\83i1,⫱*[â\86\91n]gâ¦\84 ≘ i2 & ↑(n+i2) = j2.
+lemma at_inv_nxx: â\88\80n,g,i1,j2. @â\9dªâ\86\91i1,gâ\9d« â\89\98 j2 â\86\92 @â\9dª0,gâ\9d« ≘ n →
+ â\88\83â\88\83i2. @â\9dªi1,⫱*[â\86\91n]gâ\9d« ≘ i2 & ↑(n+i2) = j2.
#n elim n -n
[ #g #i1 #j2 #Hg #H
elim (at_inv_pxp … H) -H [ |*: // ] #f #H0
]
qed-.
-lemma at_inv_tls: â\88\80i2,i1,f. @â¦\83i1,fâ¦\84 ≘ i2 → ⫯⫱*[↑i2]f ≡ ⫱*[i2]f.
+lemma at_inv_tls: â\88\80i2,i1,f. @â\9dªi1,fâ\9d« ≘ 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/
(* Advanced inversion lemmas on isid ****************************************)
-lemma isid_inv_at: â\88\80i,f. ð\9d\90\88â¦\83fâ¦\84 â\86\92 @â¦\83i,fâ¦\84 ≘ i.
+lemma isid_inv_at: â\88\80i,f. ð\9d\90\88â\9dªfâ\9d« â\86\92 @â\9dªi,fâ\9d« ≘ i.
#i elim i -i
[ #f #H elim (isid_inv_gen … H) -H /2 width=2 by at_refl/
| #i #IH #f #H elim (isid_inv_gen … H) -H /3 width=7 by at_push/
]
qed.
-lemma isid_inv_at_mono: â\88\80f,i1,i2. ð\9d\90\88â¦\83fâ¦\84 â\86\92 @â¦\83i1,fâ¦\84 ≘ i2 → i1 = i2.
+lemma isid_inv_at_mono: â\88\80f,i1,i2. ð\9d\90\88â\9dªfâ\9d« â\86\92 @â\9dªi1,fâ\9d« ≘ i2 → i1 = i2.
/3 width=6 by isid_inv_at, at_mono/ qed-.
(* Advanced properties on isid **********************************************)
-corec lemma isid_at: â\88\80f. (â\88\80i. @â¦\83i,fâ¦\84 â\89\98 i) â\86\92 ð\9d\90\88â¦\83fâ¦\84.
+corec lemma isid_at: â\88\80f. (â\88\80i. @â\9dªi,fâ\9d« â\89\98 i) â\86\92 ð\9d\90\88â\9dªfâ\9d«.
#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/
(* Advanced properties on id ************************************************)
-lemma id_inv_at: â\88\80f. (â\88\80i. @â¦\83i,fâ¦\84 ≘ i) → 𝐈𝐝 ≡ f.
+lemma id_inv_at: â\88\80f. (â\88\80i. @â\9dªi,fâ\9d« ≘ i) → 𝐈𝐝 ≡ f.
/3 width=1 by isid_at, eq_id_inv_isid/ qed-.
-lemma id_at: â\88\80i. @â¦\83i,ð\9d\90\88ð\9d\90\9dâ¦\84 ≘ i.
+lemma id_at: â\88\80i. @â\9dªi,ð\9d\90\88ð\9d\90\9dâ\9d« ≘ i.
/2 width=1 by isid_inv_at/ qed.
(* Advanced forward lemmas on id ********************************************)
-lemma at_id_fwd: â\88\80i1,i2. @â¦\83i1,ð\9d\90\88ð\9d\90\9dâ¦\84 ≘ i2 → i1 = i2.
+lemma at_id_fwd: â\88\80i1,i2. @â\9dªi1,ð\9d\90\88ð\9d\90\9dâ\9d« ≘ i2 → i1 = i2.
/2 width=4 by at_mono/ qed.
(* Main properties on id ****************************************************)
(* Properties with uniform relocations **************************************)
-lemma at_uni: â\88\80n,i. @â¦\83i,ð\9d\90\94â\9d´nâ\9dµâ¦\84 ≘ n+i.
+lemma at_uni: â\88\80n,i. @â\9dªi,ð\9d\90\94â\9d¨nâ\9d©â\9d« ≘ n+i.
#n elim n -n /2 width=5 by at_next/
qed.
(* Inversion lemmas with uniform relocations ********************************)
-lemma at_inv_uni: â\88\80n,i,j. @â¦\83i,ð\9d\90\94â\9d´nâ\9dµâ¦\84 ≘ j → j = n+i.
+lemma at_inv_uni: â\88\80n,i,j. @â\9dªi,ð\9d\90\94â\9d¨nâ\9d©â\9d« ≘ j → j = n+i.
/2 width=4 by at_mono/ qed-.