update in ground and static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / drops_sex.ma

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 d9a9588a346a996138c2c8edcda6c6a8f9123284..aeff28ceeda71426dc782d6ea008e1d5b2e11c4a 100644 (file)
--- 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.
-      (â\88\80g,I,K,n. â\87©[n] L1 â\89\98 K.â\93\98[I] â\86\92 â\86\91g = ⫱*[n] f1 → R_pw_confluent1_sex R1 R1 R2 cfull g K I) →
+      (â\88\80g,I,K,n. â\87©[n] L1 â\89\98 K.â\93\98[I] â\86\92 â\86\91g = â«°*[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