nrewrite now working

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 4fac05b51c6e2926fdaa85f21e9edc8db03561a0..40400378dc7e1bedf9b2480823f9127a93df7d2b 100644 (file)
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -73,20 +73,17 @@ ndefinition sub_magma ≝
 ndefinition image: ∀A,B. (A → B) → Ω \sup A → Ω \sup B ≝
  λA,B,f,Sa. {y | ∃x. x ∈ Sa ∧ f x = y}.
 
-naxiom daemon: False.
-
 ndefinition mm_image:
  ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma B.
  #A; #B; #Ma; #Mb; #f;
  napply (mk_magma ???)
-  [ napply (image ?? (mmcarr ?? (mmmcarr ???? f)) Ma) (* NO COMPOSITE! *)
+  [ napply (image ?? f Ma)
   | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
     napply (ex_intro ????)
      [ napply (op ? x0 y0) 
      | napply (conj ????)
         [ napply (op_closed ??????); nassumption
-        | (* nrewrite < Hx1; DOES NOT WORK *)
-          napply (eq_rect ?? (λ_.?) ?? Hx1);
-          napply (eq_rect ?? (λ_.?) ?? Hy1);
+        | nrewrite < Hx1;
+          nrewrite < Hy1;
           napply (mmprop ?? f ??)]##]
 nqed.
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index 2aca2bbd3078267429f6b195842bd37d9ecf393c..379c5765687f7478898145121db5d7351ded0e1a 100644 (file)
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -1,7 +1,6 @@
 sets/sets.ma logic/equality.ma
 topology/igt.ma logic/connectives.ma properties/relations.ma
 logic/equality.ma logic/connectives.ma
-.unnamed.ma logic/pts.ma
 logic/connectives.ma logic/pts.ma
 algebra/magmas.ma sets/sets.ma
 properties/relations.ma logic/pts.ma

diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot
index 8898c6c2e225b96c89b4ec44118ee67880340f5c..9069f0cd915dbfa0d27272e2afc85fd2523761c5 100644 (file)
--- a/helm/software/matita/nlibrary/depends.dot
+++ b/helm/software/matita/nlibrary/depends.dot
@@ -6,8 +6,6 @@ digraph g {
   "topology/igt.ma" -> "properties/relations.ma" [];
   "logic/equality.ma" [];
   "logic/equality.ma" -> "logic/connectives.ma" [];
-  ".unnamed.ma" [];
-  ".unnamed.ma" -> "logic/pts.ma" [];
   "logic/connectives.ma" [];
   "logic/connectives.ma" -> "logic/pts.ma" [];
   "algebra/magmas.ma" [];

diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png
index 6d8cfcfd912a8c417bf5b863cb08cd0dc2b086c2..c00871d4a589e1cced08f82fdd0458506696e528 100644 (file)
Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ

diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index 2418f2a7c504da2a7f8b68957604c30ad224a4be..1da7e1b0be4ec611643009b61780a08a09505cd8 100644 (file)
--- a/helm/software/matita/nlibrary/logic/equality.ma
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -17,11 +17,6 @@ include "logic/connectives.ma".
 ninductive eq (A: Type) (a: A) : A → CProp ≝
  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 ].
- 
 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)).