X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fdeqsets.ma;h=c17db5dc0cb4b1e899ae76533a686ad5322fb450;hb=cfccf434a57e10848d74d06674af4ec9cef0f0ca;hp=fb6ad5be4fe3f11a678f11e62cea79b14ba8cfb6;hpb=5d54a6d3a0f22bb8784387c491de7bb66e67b625;p=helm.git

diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index fb6ad5be4..c17db5dc0 100644
--- a/matita/matita/lib/basics/deqsets.ma
+++ b/matita/matita/lib/basics/deqsets.ma
@@ -14,11 +14,12 @@ include "basics/bool.ma".
 
 (****** DeqSet: a set with a decidbale equality ******)
 
-record DeqSet : Type[1] ≝ { carr :> Type[0];
+record DeqSet : Type[1] ≝ { 
+   carr :> Type[0];
    eqb: carr → carr → bool;
    eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
 }.
-
+    
 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
 interpretation "eqb" 'eqb a b = (eqb ? a b).