more theory for lists

[helm.git] / helm / software / matita / nlibrary / datatypes / list-setoids.ma

diff --git a/helm/software/matita/nlibrary/datatypes/list-setoids.ma b/helm/software/matita/nlibrary/datatypes/list-setoids.ma
index c836f4bf39a47bcce230c558fa89f7fa715323bd..6a1532562e00f3f02c75e9374e27c9b8a04ae879 100644 (file)
--- a/helm/software/matita/nlibrary/datatypes/list-setoids.ma
+++ b/helm/software/matita/nlibrary/datatypes/list-setoids.ma
@@ -36,13 +36,13 @@ unification hint 0 ≔ S : setoid;
   P1 ≟ refl ? (eq0 (LIST S)),
   P2 ≟ sym ? (eq0 (LIST S)),
   P3 ≟ trans ? (eq0 (LIST S)),
-  X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list T) P1 P2 P3)
+  X ≟ mk_setoid (list (carr S)) (mk_equivalence_relation ? (eq_list S) P1 P2 P3)
 (*-----------------------------------------------------------------------*) ⊢
      carr X ≡ list T.
 
-unification hint 0 ≔ S:setoid,a,b:list S;
+unification hint 0 ≔ S:setoid, a,b:list (carr S);
    R ≟ eq0 (LIST S),
-   L ≟ (list S)
+   L ≟ (list (carr S))
 (* -------------------------------------------- *) ⊢
    eq_list S a b ≡ eq_rel L R a b.
 
@@ -53,13 +53,15 @@ nlemma append_is_morph : ∀A:setoid.(list A) ⇒_0 (list A) ⇒_0 (list A).
 nqed.
 
 alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
-unification hint 0 ≔ S:setoid, A,B:list S;
-    MM ≟ mk_unary_morphism ??
-          (λA:list S.mk_unary_morphism ?? (λB:list S.A @ B) (prop1 ?? (append_is_morph S A)))
+unification hint 0 ≔ S:setoid, A,B:list (carr S);
+    SS ≟ carr S,
+    MM ≟ mk_unary_morphism ?? (λA:list (carr S).
+            mk_unary_morphism ?? 
+              (λB:list (carr S).A @ B) (prop1 ?? (fun1 ??(append_is_morph S) A)))
           (prop1 ?? (append_is_morph S)),
     T ≟ LIST S
 (*--------------------------------------------------------------------------*) ⊢
-   fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ A @ B.
+   fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ append SS A B.
 
 
 (* XXX to understand if are always needed or only if the coercion is active *)