X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FRELATIONAL%2FBEq%2Fdefs.ma;h=d851a6b9fda2a98e45b90f067c7a140c229a0907;hb=883affb9b633393615ce3cb674834664c5b9c881;hp=0b52af116a59c63f0a89c3f0ca05cbf14fa46e8e;hpb=1e8c961814b55b806652b8b8243d6f56108bda9c;p=helm.git

diff --git a/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma b/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma
index 0b52af116..d851a6b9f 100644
--- a/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma
+++ b/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma
@@ -19,6 +19,14 @@ include "logic/equality.ma".
 include "BNot/defs.ma".
 
 inductive BEq (b1:Bool): Bool \to Bool \to Prop \def
-   | beq_false: \forall b2. BNot b1 b2 \to BEq b1 false b2
+   | beq_false: \forall b2. (~b1 == b2) \to BEq b1 false b2
    | beq_true : BEq b1 true b1
 .
+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "boolean coimplication predicate" 'rel_coimp x y z = 
+   (cic:/matita/RELATIONAL/BEq/defs/BEq.ind#xpointer(1/1) x y z).
+
+notation "hvbox(a break * b break == c)" 
+  non associative with precedence 95
+for @{ 'rel_coimp $a $b $c}.