]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/syntax/item_sh.ma
renaming in basic_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / syntax / item_sh.ma
index d51bd19591b20a1700b8cff5cd86c5fc3e1ffd07..9e0b03f735e7f0f16cf87d4f144fccdeab0338de 100644 (file)
@@ -33,7 +33,7 @@ lapply (next_lt h ((next h)^n s)) #H
 lapply (le_to_lt_to_lt … IH H) -IH -H /2 width=2 by lt_to_le/
 qed.
 
-lemma nexts_lt: â\88\80h,s,n. s < (next h)^(⫯n) s.
+lemma nexts_lt: â\88\80h,s,n. s < (next h)^(â\86\91n) s.
 #h #s #n normalize
 lapply (nexts_le h s n) #H
 @(le_to_lt_to_lt … H) //