X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fs_transition%2Ffquq_length.ma;h=78d450b32df29a15b9934cd2c59dcd8b8d608dfb;hb=cc178d85bc4fec05b6a9dd176f338b3275beb3d9;hp=ed038771f6d204bad9a40b02f74418e315673af1;hpb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_length.ma b/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_length.ma
index ed038771f..78d450b32 100644
--- a/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_length.ma
@@ -19,7 +19,7 @@ include "static_2/s_transition/fquq.ma".
 
 (* Forward lemmas with length for local environments ************************)
 
-lemma fquq_fwd_length_lref1: ∀b,G1,G2,L1,L2,T2,i. ❪G1,L1,#i❫ ⬂⸮[b] ❪G2,L2,T2❫ →
+lemma fquq_fwd_length_lref1: ∀b,G1,G2,L1,L2,T2,i. ❨G1,L1,#i❩ ⬂⸮[b] ❨G2,L2,T2❩ →
                              |L2| ≤ |L1|.
 #b #G1 #G2 #L1 #L2 #T2 #i #H elim H -H [2: * ]
 /3 width=6 by fqu_fwd_length_lref1, nlt_des_le/