notational update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfxs_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
index 40ce94c71227cb3a5a72492d04311a61a63d2985..c37c2d3462f4115a0b33542905638bb77f247dfd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
@@ -36,7 +36,7 @@ definition dropable_dx: predicate (relation3 lenv term term) ≝
 
 definition lfxs_transitive_next: relation3 … ≝ λR1,R2,R3.
                                  ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≘ f →
-                                 â\88\80g,I,K,n. â¬\87*[n] L â\89\98 K.â\93\98{I} â\86\92 ⫯g = ⫱*[n] f →
+                                 â\88\80g,I,K,n. â¬\87*[n] L â\89\98 K.â\93\98{I} â\86\92 â\86\91g = ⫱*[n] f →
                                  lexs_transitive (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I.
 
 (* Properties with generic slicing for local environments *******************)