X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fequality.ma;h=715423143e7185debaf41b69046ba5e1ccde202b;hb=99c0c1171257384a8d9c1910a3b123fe91bfe29c;hp=2418f2a7c504da2a7f8b68957604c30ad224a4be;hpb=6003ba0e4600778c6055ed5ea5cb6c1fba3abe32;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index 2418f2a7c..715423143 100644
--- a/helm/software/matita/nlibrary/logic/equality.ma
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -13,15 +13,29 @@
 (**************************************************************************)
 
 include "logic/connectives.ma".
+include "properties/relations.ma".
 
-ninductive eq (A: Type) (a: A) : A → CProp ≝
+ninductive eq (A: Type[0]) (a: A) : A → CProp[0] ≝
  refl: eq A a a.
 
-nlet rec eq_rect (A: Type) (x: A) (P: ∀y:A. eq A x y → CProp) (q: P x (refl A x))
- (y: A) (p: eq A x y) on p : P y p ≝
- match p with
-  [ refl ⇒ q ].
- 
+nlemma eq_rect_CProp0_r':
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
+ #A; #a; #x; #p; ncases p; #P; #H; nassumption.
+nqed.
+
+nlemma eq_rect_CProp0_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
+nqed.
+
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
+
+ndefinition EQ: ∀A:Type[0]. equivalence_relation A.
+ #A; napply mk_equivalence_relation
+  [ napply eq
+  | napply refl
+  | #x; #y; #H; nrewrite < H; napply refl
+  | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption]
+nqed.