update in ground and static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / rex_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma
index dba0cb30be483d6957b4bf91a8009f39b1189b56..b6374ac0b04edbdd5bbe445b8c16e038b79282fa 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma
@@ -40,12 +40,12 @@ definition f_dropable_dx:
 definition f_transitive_next:
            relation3 … ≝ λR1,R2,R3.
            ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f →
-           â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = ⫱*[i] f →
+           â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = â«°*[i] f →
            R_pw_transitive_sex (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I.
 
 definition f_confluent1_next: relation2 … ≝ λR1,R2.
            ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f →
-           â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = ⫱*[i] f →
+           â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = â«°*[i] f →
            R_pw_confluent1_sex (cext2 R1) (cext2 R1) (cext2 R2) cfull g K I.
 
 (* Properties with generic slicing for local environments *******************)