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

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma
index d9a9588a3..aeff28cee 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma
@@ -198,7 +198,7 @@ qed-.
 lemma sex_sdj_split_dx (R1) (R2) (RP):
       c_reflexive … R1 → c_reflexive … R2 → c_reflexive … RP →
       ∀L1,f1.
-      (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f1 → R_pw_confluent1_sex R1 R1 R2 cfull g K I) →
+      (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫰*[n] f1 → R_pw_confluent1_sex R1 R1 R2 cfull g K I) →
       ∀L2. L1 ⪤[R1,RP,f1] L2 → ∀f2. f1 ∥ f2 →
       ∃∃L. L1 ⪤[R2,cfull,f1] L & L ⪤[RP,R1,f2] L2.
 #R1 #R2 #RP #HR1 #HR2 #HRP #L1 elim L1 -L1