(**************************************************************************)
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.
-
+
+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; #x; #p; #x0; #p0; napply eq_rect_CProp0_r'; 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.