X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fsex.ma;h=2a6946fcab7ac6441c2109b34fbdfa422e9b625c;hp=72909212ca0f9bcbdc72968302e0932542730623;hb=dc605ae41c39773f55381f241b1ed3db4acf5edd;hpb=caf822cbe34e204e6d1b72e272373b561c1a565a

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma
index 72909212c..2a6946fca 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma
@@ -177,7 +177,7 @@ lemma sex_inv_push (RN) (RP):
 qed-.
 
 lemma sex_inv_tl (RN) (RP):
-      ∀f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫱f] L2 →
+      ∀f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫰f] L2 →
       RN L1 I1 I2 → RP L1 I1 I2 →
       L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2].
 #RN #RP #f #I1 #I2 #L2 #L2 elim (pn_split f) *
@@ -188,7 +188,7 @@ qed-.
 
 lemma sex_fwd_bind (RN) (RP):
       ∀f,I1,I2,L1,L2.
-      L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → L1 ⪤[RN,RP,⫱f] L2.
+      L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → L1 ⪤[RN,RP,⫰f] L2.
 #RN #RP #f #I1 #I2 #L1 #L2 #Hf
 elim (pn_split f) * #g #H destruct
 [ elim (sex_inv_push … Hf) | elim (sex_inv_next … Hf) ] -Hf //
@@ -330,7 +330,7 @@ lemma sex_dec (RN) (RP):
   lapply (sex_inv_atom1 … H) -H #H destruct
 | #f @or_intror #H
   lapply (sex_inv_atom2 … H) -H #H destruct
-| #L2 #I2 #f elim (IH L2 (⫱f)) -IH #HL12
+| #L2 #I2 #f elim (IH L2 (â«°f)) -IH #HL12
   [2: /4 width=3 by sex_fwd_bind, or_intror/ ]
   elim (pn_split f) * #g #H destruct
   [ elim (HRP L1 I1 I2) | elim (HRN L1 I1 I2) ] -HRP -HRN #HV12