Some results on relations. Moved things around.

[helm.git] / matita / matita / lib / basics / deqsets.ma

diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index dc0044edc08efed553791e47ab5862e989a9350f..fcc89f3127007036a20a4b09e62b9b72d3bd0570 100644 (file)
--- 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).