]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/static_2/static/feqg_length.ma
update in ground static_2 basic_2 apps_2
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / feqg_length.ma
index fd4119f87ce4844f2dbaab6ac82fae69957ca3c4..b6a308648774ec391e47326c78137d593ebff4b4 100644 (file)
@@ -20,5 +20,5 @@ include "static_2/static/feqg.ma".
 (* Forward lemmas with length for local environments ************************)
 
 lemma feqg_fwd_length (S) (G1) (G2) (L1) (L2) (T1) (T2):
-      â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG2,L2,T2â\9d« → |L1| = |L2|.
+      â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G2,L2,T2â\9d© → |L1| = |L2|.
 /3 width=6 by feqg_fwd_reqg_sn, reqg_fwd_length/ qed-.