renaming in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
index c119905ceca9adac050a7eaa63853eebed764501..6ea5a39c40b289f7ee55ddc69b2bcec459187602 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
@@ -23,7 +23,7 @@ include "basic_2/syntax/genv.ma".
 inductive aaa: relation4 genv lenv term aarity ≝
 | aaa_sort: ∀G,L,s. aaa G L (⋆s) (⓪)
 | aaa_zero: ∀I,G,L,V,B. aaa G L V B → aaa G (L.ⓑ{I}V) (#0) B
-| aaa_lref: â\88\80I,G,L,A,i. aaa G L (#i) A â\86\92 aaa G (L.â\93\98{I}) (#⫯i) A
+| aaa_lref: â\88\80I,G,L,A,i. aaa G L (#i) A â\86\92 aaa G (L.â\93\98{I}) (#â\86\91i) A
 | aaa_abbr: ∀p,G,L,V,T,B,A.
             aaa G L V B → aaa G (L.ⓓV) T A → aaa G L (ⓓ{p}V.T) A
 | aaa_abst: ∀p,G,L,V,T,B,A.
@@ -67,7 +67,7 @@ lemma aaa_inv_zero: ∀G,L,A. ⦃G, L⦄ ⊢ #0 ⁝ A →
                     ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ⁝ A.
 /2 width=3 by aaa_inv_zero_aux/ qed-.
 
-fact aaa_inv_lref_aux: â\88\80G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â\88\80i. T = #(⫯i) →
+fact aaa_inv_lref_aux: â\88\80G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â\88\80i. T = #(â\86\91i) →
                        ∃∃I,K. L = K.ⓘ{I} & ⦃G, K⦄ ⊢ #i ⁝ A.
 #G #L #T #A * -G -L -T -A
 [ #G #L #s #j #H destruct
@@ -80,7 +80,7 @@ fact aaa_inv_lref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀i. T = #(⫯i)
 ]
 qed-.
 
-lemma aaa_inv_lref: â\88\80G,L,A,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i ⁝ A →
+lemma aaa_inv_lref: â\88\80G,L,A,i. â¦\83G, Lâ¦\84 â\8a¢ #â\86\91i ⁝ A →
                     ∃∃I,K. L = K.ⓘ{I} & ⦃G, K⦄ ⊢ #i ⁝ A.
 /2 width=3 by aaa_inv_lref_aux/ qed-.