X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Faaa_reqx.ma;h=c3a6249e156f869d92160ed8f689b8fceaa325c7;hp=b502a8a2701cc946577fa59e286c26551237634f;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa_reqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa_reqx.ma
index b502a8a27..c3a6249e1 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/aaa_reqx.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa_reqx.ma
@@ -19,8 +19,8 @@ include "static_2/static/aaa.ma".
 
 (* Properties with sort-irrelevant equivalence on referred entries **********)
 
-lemma aaa_teqx_conf_reqx: ∀G,L1,T1,A. ⦃G,L1⦄ ⊢ T1 ⁝ A → ∀T2. T1 ≛ T2 →
-                          ∀L2. L1 ≛[T1] L2 → ⦃G,L2⦄ ⊢ T2 ⁝ A.
+lemma aaa_teqx_conf_reqx: ∀G,L1,T1,A. ❪G,L1❫ ⊢ T1 ⁝ A → ∀T2. T1 ≛ T2 →
+                          ∀L2. L1 ≛[T1] L2 → ❪G,L2❫ ⊢ T2 ⁝ A.
 #G #L1 #T1 #A #H elim H -G -L1 -T1 -A
 [ #G #L1 #s1 #X #H1 elim (teqx_inv_sort1 … H1) -H1 //
 | #I #G #L1 #V1 #B #_ #IH #X #H1 >(teqx_inv_lref1 … H1) -H1