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

diff --git a/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma b/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma
index d851a6b9f..3ab3b002e 100644
--- a/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma
+++ b/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma
@@ -16,17 +16,17 @@ set "baseuri" "cic:/matita/RELATIONAL/BEq/defs".
 
 include "logic/equality.ma".
 
-include "BNot/defs.ma".
+include "Bool/defs.ma".
 
-inductive BEq (b1:Bool): Bool \to Bool \to Prop \def
-   | beq_false: \forall b2. (~b1 == b2) \to BEq b1 false b2
-   | beq_true : BEq b1 true b1
+inductive BEq (A:Type) (a1:A): A \to Bool \to Prop \def
+   | beq_true : BEq A a1 a1 true
+   | beq_false: \forall a2. (a1 = a2 -> False) \to BEq A a1 a2 false
 .
 
 (*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).
+interpretation "boolean equality" 'beq x y z = 
+   (cic:/matita/RELATIONAL/BEq/defs/BEq.ind#xpointer(1/1) _ x y z).
 
-notation "hvbox(a break * b break == c)" 
+notation "hvbox(a break -- b break == c)" 
   non associative with precedence 95
-for @{ 'rel_coimp $a $b $c}.
+for @{ 'beq $a $b $c}.