X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fduality.ma;h=f967a416bbf6667be79abc105a0e60e3c1fd242e;hb=eaaea3c18083de3e442e939768ff450d3b093911;hp=14927653e2a08093452ebe02c5dd7ce1cab1a335;hpb=dc66c8d89a5147178ccdacb8341ed26c9c52f06b;p=helm.git

diff --git a/matita/matita/library/didactic/exercises/duality.ma b/matita/matita/library/didactic/exercises/duality.ma
index 14927653e..f967a416b 100644
--- a/matita/matita/library/didactic/exercises/duality.ma
+++ b/matita/matita/library/didactic/exercises/duality.ma
@@ -219,7 +219,7 @@ let rec negate (F: Formula) on F : Formula ≝
 *)
 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).
 lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; rewrite < H; rewrite < H1; reflexivity. qed.
 lemma equiv_sym : ∀a,b.a ≡ b → b ≡ a. intros 4;symmetry;apply H;qed.