X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Flambda_notation.ma;h=42f3eb2aa7c3742ae656ddaa9a29bee39962378e;hb=060f4ff9bcece134dd66757ee7f8c571bdbc8cab;hp=55a75eb780ea28e6010d5c2c050474cb29458f18;hpb=87d894fbd1d1c6ae4f9a8421ffa39af838b72e9f;p=helm.git

diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index 55a75eb78..42f3eb2aa 100644
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -14,6 +14,12 @@
 
 (* NOTATION FOR THE LAMBDA CALCULUS *******************************************)
 
+(* equivalences *)
+
+notation "hvbox(a break ≅ b)" 
+  non associative with precedence 45
+  for @{'Eq $a $b}.
+
 (* lifting, substitution *)
 
 notation "hvbox(M break [ l ])"