X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fdeqsets.ma;h=fcc89f3127007036a20a4b09e62b9b72d3bd0570;hb=e37238b40356ee1b5e7859cf0eb6567918f2ebec;hp=dc0044edc08efed553791e47ab5862e989a9350f;hpb=7d58d5dc7f897622f2010326023b17c6592d5f03;p=helm.git

diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index dc0044edc..fcc89f312 100644
--- a/matita/matita/lib/basics/deqsets.ma
+++ b/matita/matita/lib/basics/deqsets.ma
@@ -114,6 +114,7 @@ unification hint  0 ≔ T,a1,a2;
 (* ---------------------------------------- *) ⊢ 
     eq_option T a1 a2 ≡ eqb X a1 a2.
 
+
 (* pairs *)
 definition eq_pairs ≝
   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).