X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfxs.ma;h=5daeedab0ca117b1c0f2aa392549e767bede594d;hb=397413c4196f84c81d61ba7dd79b54ab1c428ebb;hp=8d82750f1db9f679e65824f307e5f1e4abfe4a6e;hpb=24ba1bb3f67505d3e384747ff90d26d3996bd3f5;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index 8d82750f1..5daeedab0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -84,7 +84,7 @@ lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⪤*[R, #0] Y2 →
 ]
 qed-.
 
-lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⪤*[R, #⫯i] Y2 →
+lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⪤*[R, #↑i] Y2 →
                      ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
                       | ∃∃I1,I2,L1,L2. L1 ⪤*[R, #i] L2 &
                                        Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
@@ -183,7 +183,7 @@ lemma lfxs_inv_zero_unit_dx: ∀R,I,L1,K2. L1 ⪤*[R, #0] K2.ⓤ{I} →
 ]
 qed-.
 
-lemma lfxs_inv_lref_bind_sn: ∀R,I1,K1,L2,i. K1.ⓘ{I1} ⪤*[R, #⫯i] L2 →
+lemma lfxs_inv_lref_bind_sn: ∀R,I1,K1,L2,i. K1.ⓘ{I1} ⪤*[R, #↑i] L2 →
                              ∃∃I2,K2. K1 ⪤*[R, #i] K2 & L2 = K2.ⓘ{I2}.
 #R #I1 #K1 #L2 #i #H elim (lfxs_inv_lref … H) -H *
 [ #H destruct
@@ -191,7 +191,7 @@ lemma lfxs_inv_lref_bind_sn: ∀R,I1,K1,L2,i. K1.ⓘ{I1} ⪤*[R, #⫯i] L2 →
 ]
 qed-.
 
-lemma lfxs_inv_lref_bind_dx: ∀R,I2,K2,L1,i. L1 ⪤*[R, #⫯i] K2.ⓘ{I2} →
+lemma lfxs_inv_lref_bind_dx: ∀R,I2,K2,L1,i. L1 ⪤*[R, #↑i] K2.ⓘ{I2} →
                              ∃∃I1,K1. K1 ⪤*[R, #i] K2 & L1 = K1.ⓘ{I1}.
 #R #I2 #K2 #L1 #i #H elim (lfxs_inv_lref … H) -H *
 [ #_ #H destruct
@@ -273,7 +273,7 @@ lemma lfxs_unit: ∀R,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cext2 R, cfull, f] L2 
 /4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed.
 
 lemma lfxs_lref: ∀R,I1,I2,L1,L2,i.
-                 L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #⫯i] L2.ⓘ{I2}.
+                 L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #↑i] L2.ⓘ{I2}.
 #R #I1 #I2 #L1 #L2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/
 qed.