X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_tls_nexts_eq.ma;h=a0d4e3910c2cf7ea066c38662234f2fff83ec5e1;hb=8bbe582d87984526f40182c4409cbfd43108cb79;hp=874eab14f5fc4c8a25fdcab56ac3691aeef2571f;hpb=55c768d7e45babb300b5010463ba3196a68f1bbe;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma
index 874eab14f..a0d4e3910 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma
@@ -15,14 +15,14 @@
 include "ground/relocation/gr_nexts.ma".
 include "ground/relocation/gr_tls_eq.ma".
 
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
 
-(* Inversion lemmas with gr_nexts and gr_eq *****************************************************)
+(* Inversions with gr_nexts and gr_eq ***************************************)
 
 (*** eq_inv_nexts_sn *)
 lemma gr_eq_inv_nexts_sn (n):
       ∀f1,g2. ↑*[n] f1 ≡ g2 →
-      ∧∧ f1 ≡ ⫱*[n]g2 & ↑*[n]⫱*[n]g2 = g2.
+      ∧∧ f1 ≡ ⫰*[n]g2 & ↑*[n]⫰*[n]g2 = g2.
 #n @(nat_ind_succ … n) -n /2 width=1 by conj/
 #n #IH #f1 #g2 #H
 elim (gr_eq_inv_next_sn … H) -H [|*: // ] #Hf10 *
@@ -33,7 +33,7 @@ qed-.
 (*** eq_inv_nexts_dx *)
 lemma gr_eq_inv_nexts_dx (n):
       ∀f2,g1. g1 ≡ ↑*[n] f2 →
-      ∧∧ ⫱*[n]g1 ≡ f2 & ↑*[n]⫱*[n]g1 = g1.
+      ∧∧ ⫰*[n]g1 ≡ f2 & ↑*[n]⫰*[n]g1 = g1.
 #n @(nat_ind_succ … n) -n /2 width=1 by conj/
 #n #IH #f2 #g1 #H
 elim (gr_eq_inv_next_dx … H) -H [|*: // ] #Hf02 *