X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fsubstitution.ma;h=e55569a4be3ed65affb6ad5a321362f397d5c159;hb=f0d422b660e11886ec4f9a823da795050f07e07f;hp=db83cfef8cd43346cdfc43daf7ebaed3b442be8b;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/library/didactic/exercises/substitution.ma b/matita/matita/library/didactic/exercises/substitution.ma
index db83cfef8..e55569a4b 100644
--- a/matita/matita/library/didactic/exercises/substitution.ma
+++ b/matita/matita/library/didactic/exercises/substitution.ma
@@ -298,7 +298,7 @@ notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @
 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]v = [[ F2 ]]v.
 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
-notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
+notation > "a ≡ b" non associative with precedence 55 for @{ equiv $a $b }.
 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 
 (* Test 2