X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=fd1fb0037a1cff7c0525e3f88ed185df9b5eba08;hb=bfb1d0076c4adf923f0507e4e2ab26519e689b88;hp=3029bc0f4f7db8fa34893f4fb7444cdbf6ed237b;hpb=6820542245d3943e20cb560473db81bb93599fad;p=helm.git

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index 3029bc0f4..fd1fb0037 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -15,9 +15,8 @@
 (* Code ported from the Coq theorem prover by Claudio Sacerdoti Coen *)
 (* Original author: Claudio Sacerdoti Coen. for the Coq system       *)
 
-set "baseuri" "cic:/matita/technicalities/setoids".
-
 include "datatypes/constructors.ma".
+include "logic/coimplication.ma".
 include "logic/connectives2.ma".
 
 (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
@@ -51,42 +50,30 @@ inductive Areflexive_Relation_Class  : Type :=
  | AAsymmetric : ∀A.∀Aeq : relation A. Areflexive_Relation_Class.
 
 definition relation_class_of_argument_class : Argument_Class → Relation_Class.
- intro;
- unfold in a ⊢ %;
- elim a;
+ intros (a); cases a;
   [ apply (SymmetricReflexive ? ? ? H H1)
   | apply (AsymmetricReflexive ? something ? ? H)
   | apply (SymmetricAreflexive ? ? ? H)
   | apply (AsymmetricAreflexive ? something ? r)
-  | apply (Leibniz ? T1)
+  | apply (Leibniz ? T)
   ]
 qed.
 
 definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
- intros;
- elim x;
- [1,2,3,4,5: exact T1]
+ intros (X x); cases x (A o o o o A o o A o o o A o A); exact A.
 qed.
 
-definition relation_of_relation_class :
+definition relation_of_relation_class:
  ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
- intros 2;
- elim R 0;
- simplify;
-  [1,2: intros 4; apply r
-  |3,4: intros 3; apply r
-  | apply eq
- ]
+intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ]
 qed.
 
 lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
  ∀R.
   carrier_of_relation_class ? (relation_class_of_argument_class R) =
    carrier_of_relation_class ? R.
- intro;
- elim R;
- reflexivity.
- qed.
+intro; cases R; reflexivity.
+qed.
 
 inductive nelistT (A : Type) : Type :=
    singl : A → nelistT A
@@ -96,11 +83,10 @@ definition Arguments := nelistT Argument_Class.
 
 definition function_type_of_morphism_signature :
  Arguments → Relation_Class → Type.
-  intros (In Out);
-  elim In
-   [ exact (carrier_of_relation_class ? t → carrier_of_relation_class ? Out)
-   | exact (carrier_of_relation_class ? t → T)
-   ]
+  intros (In Out); elim In; 
+  [ exact (carrier_of_relation_class ? a → carrier_of_relation_class ? Out)
+  | exact (carrier_of_relation_class ? a → T)
+  ]
 qed. 
 
 definition make_compatibility_goal_aux:
@@ -111,31 +97,26 @@ definition make_compatibility_goal_aux:
  generalize in match f; clear f;
   [ elim a; simplify in f f1;
      [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
-     | elim t;
+     | cases x;
         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
         ]
      | exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
-     | elim t;
+     | cases x;
         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
         ]
      | exact (∀x. relation_of_relation_class ? Out (f x) (f1 x))
      ]
   | change with
-     ((carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
-      (carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
+     ((carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) →
+      (carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) →
       Prop).
-    elim t; simplify in f f1;
-     [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
-     | elim t1;
-        [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
-        | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
-        ]
-     | exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
-     | elim t1;
-        [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
-        | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
+    elim a; simplify in f f1;
+     [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
+     |2,4: cases x;
+        [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
+        |2,4: exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
         ]
      | exact (∀x. R (f x) (f1 x))
      ]
@@ -153,8 +134,8 @@ record Morphism_Theory (In: Arguments) (Out: Relation_Class) : Type :=
 definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments.
  intro;
  elim n;
-  [ apply (singl ? (Leibniz ? t))
-  | apply (cons ? (Leibniz ? t) a)
+  [ apply (singl ? (Leibniz ? a))
+  | apply (cons ? (Leibniz ? a) a1)
   ]
 qed.
 
@@ -167,14 +148,12 @@ definition morphism_theory_of_function :
     Morphism_Theory In' Out'.
   intros;
   apply (mk_Morphism_Theory ? ? f);
-  unfold In' in f; clear In';
-  unfold Out' in f; clear Out';
+  unfold In' in f ⊢ %; clear In';
+  unfold Out' in f ⊢ %; clear Out';
   generalize in match f; clear f;
   elim In;
    [ unfold make_compatibility_goal;
-     simplify;
-     intros;
-     whd;
+     whd; intros;
      reflexivity
    | simplify;
      intro;
@@ -222,13 +201,29 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation:
  apply mk_Morphism_Theory;
   [ exact Aeq
   | unfold make_compatibility_goal;
-    simplify;
+    simplify; unfold ASetoidClass; simplify;
     intros;
     split;
     unfold transitive in H;
     unfold symmetric in sym;
     intro;
-    auto new
+      [ apply (H x2 x1 x3 ? ?);
+          [apply (sym x1 x2 ?).
+           apply (H1).
+          |apply (H x1 x x3 ? ?);
+            [apply (H3).
+            |apply (H2).
+            ]
+          ]
+      | apply (H x1 x3 x ? ?);
+         [apply (H x1 x2 x3 ? ?);
+            [apply (H1).
+            |apply (H3).
+            ]
+         |apply (sym x x3 ?).
+          apply (H2).
+         ]
+      ]
   ].
 qed.
 
@@ -239,14 +234,33 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation:
     (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class).
  intros;
  apply mk_Morphism_Theory;
- reduce;
+ normalize;
   [ exact Aeq
   | intros;
     split;
     intro;
     unfold transitive in H;
     unfold symmetric in sym;
-    auto depth=4.
+    [ apply (H x2 x1 x3 ? ?);
+        [apply (sym x1 x2 ?).
+         apply (H1).
+        |apply (H x1 x x3 ? ?);
+          [apply (H3).
+          |apply (H2).
+          ]
+        ]
+    | apply (H x1 x2 x ? ?);
+      [apply (H1).
+      |apply (H x2 x3 x ? ?);
+        [apply (H3).
+        |apply (sym x x3 ?).
+         apply (H x x3 x3 ? ?);
+          [apply (H2).
+          |apply (refl x3).
+          ]
+        ]
+      ]
+    ]
   ]
 qed.
 
@@ -259,11 +273,17 @@ definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
  apply mk_Morphism_Theory;
  [ simplify;
    apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
    intros;
    whd;
    intros;
-   auto
+   apply (H x2 x1 x3 ? ?);
+    [apply (H1).
+    |apply (H x1 x x3 ? ?);
+      [apply (H3).
+      |apply (H2).
+      ]
+    ]
  ].
 qed.
 
@@ -276,11 +296,17 @@ definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
  apply mk_Morphism_Theory;
  [ simplify;
    apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
    intros;
    whd;
    intro;
-   auto
+   apply (H x2 x1 x3 ? ?);
+     [apply (H1).
+     |apply (H x1 x x3 ? ?);
+       [apply (H3).
+       |apply (H2).
+       ]
+     ]
  ].
 qed.
 
@@ -304,9 +330,8 @@ definition morphism_theory_of_predicate :
   | generalize in match f; clear f;
     unfold In'; clear In';
     elim In;
-     [ reduce;
+     [ normalize;
        intro;
-       alias id "iff_refl" = "cic:/matita/logic/coimplication/iff_refl.con".
        apply iff_refl
      | simplify;
        intro x;
@@ -321,7 +346,8 @@ theorem impl_trans: transitive ? impl.
  whd;
  unfold impl;
  intros;
- auto.
+ apply (H1 ?).apply (H ?).apply (H2).
+ autobatch.
 qed.
 
 (*DA PORTARE: Add Relation Prop impl
@@ -339,9 +365,9 @@ definition variance_of_argument_class : Argument_Class → option variance.
  intros;
  elim a;
   [ apply None
-  | apply (Some ? t)
+  | apply (Some ? x)
   | apply None
-  | apply (Some ? t)
+  | apply (Some ? x)
   | apply None
   ]
 qed.
@@ -401,7 +427,7 @@ inductive Morphism_Context (Hole: Relation_Class) (dir:rewrite_direction) : Rela
     App :
       ∀In,Out,dir'.
         Morphism_Theory In Out → Morphism_Context_List Hole dir dir' In →
-           Morphism_Context Hole dir Out dir
+           Morphism_Context Hole dir Out dir'
   | ToReplace : Morphism_Context Hole dir Hole dir
   | ToKeep :
      ∀S,dir'.
@@ -426,17 +452,129 @@ with Morphism_Context_List :
          Morphism_Context_List Hole dir dir'' L →
           Morphism_Context_List Hole dir dir'' (cons ? S L).
 
+lemma Morphism_Context_rect2:
+ ∀Hole,dir.
+ ∀P:
+  ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
+ ∀P0:
+  ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
+ (∀In,Out,dir'.
+   ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
+    P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
+ P Hole dir (ToReplace Hole dir) →
+ (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
+   P (relation_class_of_reflexive_relation_class S) dir'
+    (ToKeep Hole dir S dir' c)) →
+ (∀S:Areflexive_Relation_Class.∀dir'.
+   ∀x:carrier_of_areflexive_relation_class S.
+    ∀r:relation_of_areflexive_relation_class S x x.
+     P (relation_class_of_areflexive_relation_class S) dir'
+      (ProperElementToKeep Hole dir S dir' x r)) →
+ (∀S:Argument_Class.∀dir',dir''.
+   ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
+    ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
+     P (relation_class_of_argument_class S) dir' m ->
+      P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
+ (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
+   ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
+    ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
+     P (relation_class_of_argument_class S) dir' m →
+      ∀m0:Morphism_Context_List Hole dir dir'' L.
+       P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
+ ∀r:Relation_Class.∀r0:rewrite_direction.∀m:Morphism_Context Hole dir r r0.
+  P r r0 m
+≝
+ λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
+ let rec
+  F (rc:Relation_Class) (r0:rewrite_direction)
+   (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
+ ≝
+  match m return λrc.λr0.λm0.P rc r0 m0 with
+  [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
+  | ToReplace ⇒ f0
+  | ToKeep S dir' c ⇒ f1 S dir' c
+  | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
+  ]
+ and
+  F0 (r:rewrite_direction) (a:Arguments)
+   (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
+ ≝
+  match m return λr.λa.λm0.P0 r a m0 with
+  [ fcl_singl S dir' dir'' c m0 ⇒
+      f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
+  | fcl_cons S L dir' dir'' c m0 m1 ⇒
+      f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
+        m1 (F0 dir'' L m1)
+  ]
+in F.
+
+lemma Morphism_Context_List_rect2:
+ ∀Hole,dir.
+ ∀P:
+  ∀r:Relation_Class.∀r0:rewrite_direction.Morphism_Context Hole dir r r0 → Type.
+ ∀P0:
+  ∀r:rewrite_direction.∀a:Arguments.Morphism_Context_List Hole dir r a → Type.
+ (∀In,Out,dir'.
+   ∀m:Morphism_Theory In Out.∀m0:Morphism_Context_List Hole dir dir' In.
+    P0 dir' In m0 → P Out dir' (App Hole ? ? ? ? m m0)) →
+ P Hole dir (ToReplace Hole dir) →
+ (∀S:Reflexive_Relation_Class.∀dir'.∀c:carrier_of_reflexive_relation_class S.
+   P (relation_class_of_reflexive_relation_class S) dir'
+    (ToKeep Hole dir S dir' c)) →
+ (∀S:Areflexive_Relation_Class.∀dir'.
+   ∀x:carrier_of_areflexive_relation_class S.
+    ∀r:relation_of_areflexive_relation_class S x x.
+     P (relation_class_of_areflexive_relation_class S) dir'
+      (ProperElementToKeep Hole dir S dir' x r)) →
+ (∀S:Argument_Class.∀dir',dir''.
+   ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
+    ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
+     P (relation_class_of_argument_class S) dir' m ->
+      P0 dir'' (singl ? S) (fcl_singl ? ? S ? ? c m)) →
+ (∀S:Argument_Class.∀L:Arguments.∀dir',dir''.
+   ∀c:check_if_variance_is_respected (variance_of_argument_class S) dir' dir''.
+    ∀m:Morphism_Context Hole dir (relation_class_of_argument_class S) dir'.
+     P (relation_class_of_argument_class S) dir' m →
+      ∀m0:Morphism_Context_List Hole dir dir'' L.
+       P0 dir'' L m0 → P0 dir'' (cons ? S L) (fcl_cons ? ? S ? ? ? c m m0)) →
+ ∀r:rewrite_direction.∀a:Arguments.∀m:Morphism_Context_List Hole dir r a.
+  P0 r a m
+≝
+ λHole,dir,P,P0,f,f0,f1,f2,f3,f4.
+ let rec
+  F (rc:Relation_Class) (r0:rewrite_direction)
+   (m:Morphism_Context Hole dir rc r0) on m : P rc r0 m
+ ≝
+  match m return λrc.λr0.λm0.P rc r0 m0 with
+  [ App In Out dir' m0 m1 ⇒ f In Out dir' m0 m1 (F0 dir' In m1)
+  | ToReplace ⇒ f0
+  | ToKeep S dir' c ⇒ f1 S dir' c
+  | ProperElementToKeep S dir' x r1 ⇒ f2 S dir' x r1
+  ]
+ and
+  F0 (r:rewrite_direction) (a:Arguments)
+   (m:Morphism_Context_List Hole dir r a) on m : P0 r a m
+ ≝
+  match m return λr.λa.λm0.P0 r a m0 with
+  [ fcl_singl S dir' dir'' c m0 ⇒
+      f3 S dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
+  | fcl_cons S L dir' dir'' c m0 m1 ⇒
+      f4 S L dir' dir'' c m0 (F (relation_class_of_argument_class S) dir' m0)
+        m1 (F0 dir'' L m1)
+  ]
+in F0.
+
 definition product_of_arguments : Arguments → Type.
  intro;
  elim a;
-  [ apply (carrier_of_relation_class ? t)
-  | apply (Prod (carrier_of_relation_class ? t) T)
+  [ apply (carrier_of_relation_class ? a1)
+  | apply (Prod (carrier_of_relation_class ? a1) T)
   ]
 qed.
 
 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
  intros (dir R);
- cases (variance_of_argument_class R);
+ cases (variance_of_argument_class R) (a);
   [ exact dir
   | cases a;
      [ exact dir                      (* covariant *)
@@ -458,17 +596,12 @@ qed.
 definition directed_relation_of_argument_class:
  ∀dir:rewrite_direction.∀R: Argument_Class.
    carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
-  intros (dir R);
-  generalize in match
-   (about_carrier_of_relation_class_and_relation_class_of_argument_class R);
-  intro H;
-  apply (directed_relation_of_relation_class dir (relation_class_of_argument_class R));
-  apply (eq_rect ? ? (λX.X) ? ? (sym_eq ? ? ? H));
-   [ apply c
-   | apply c1
-   ]
+  intros (dir R c c1);
+  rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class R) in c c1;
+  exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)  c c1).
 qed.
 
+
 definition relation_of_product_of_arguments:
  ∀dir:rewrite_direction.∀In.
   product_of_arguments In → product_of_arguments In → Prop.
@@ -476,16 +609,16 @@ definition relation_of_product_of_arguments:
  elim In 0;
   [ simplify;
     intro;
-    exact (directed_relation_of_argument_class (get_rewrite_direction r t) t)
+    exact (directed_relation_of_argument_class (get_rewrite_direction r a) a)
   | intros;
-    change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
-    change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
-    cases p;
-    cases p1;
+    change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
+    change in p1 with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
+    cases p (c p2);
+    cases p1 (c1 p3);
    apply And;
     [ exact
-      (directed_relation_of_argument_class (get_rewrite_direction r t) t a a1)
-    | exact (R b b1)
+      (directed_relation_of_argument_class (get_rewrite_direction r a) a c c1)
+    | exact (R p2 p3)
     ]
   ]
 qed. 
@@ -496,10 +629,10 @@ definition apply_morphism:
  intro;
  elim In;
   [ exact (f p)
-  | change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
+  | change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
    elim p;
-   change in f1 with (carrier_of_relation_class variance t → function_type_of_morphism_signature n Out);
-   exact (f ? (f1 t1) t2)
+   change in f1 with (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out);
+   exact (f ? (f1 a1) b)
   ]
 qed.
 
@@ -516,33 +649,28 @@ theorem apply_morphism_compatibility_Right2Left:
    [ simplify in m1 m2 args1 args2 ⊢ %;
      change in H1 with
       (directed_relation_of_argument_class
-        (get_rewrite_direction Right2Left t) t args1 args2);
+        (get_rewrite_direction Right2Left a) a args1 args2);
      generalize in match H1; clear H1;
      generalize in match H; clear H;
      generalize in match args2; clear args2;
      generalize in match args1; clear args1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim a 0; simplify;
       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
-        simplify in H;
-        simplify in H1;
-        simplify;
         apply H;
         exact H1
       | intros 8 (v T1 r Hr m1 m2 args1 args2);
-        cases v;
+        cases v; 
+        simplify;
         intros (H H1);
-        simplify in H1;
-        apply H;
-        exact H1
+        apply (H ? ? H1);
       | intros;
         apply H1;
         exact H2
       | intros 7 (v);
-        cases v;
+        cases v; simplify;
         intros (H H1);
-        simplify in H1;
         apply H;
         exact H1
       | intros;
@@ -552,74 +680,51 @@ theorem apply_morphism_compatibility_Right2Left:
         exact H1
       ]
    | change in m1 with
-      (carrier_of_relation_class variance t →
+      (carrier_of_relation_class variance a →
         function_type_of_morphism_signature n Out);
      change in m2 with
-      (carrier_of_relation_class variance t →
+      (carrier_of_relation_class variance a →
         function_type_of_morphism_signature n Out);
      change in args1 with
-      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
      change in args2 with
-      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
      generalize in match H2; clear H2;
      elim args2 0; clear args2;
      elim args1; clear args1;
+     simplify in H2;
+     change in H2:(? ? %) with 
+       (relation_of_product_of_arguments Right2Left n b b1);
      elim H2; clear H2;
-     change in H4 with
-      (relation_of_product_of_arguments Right2Left n t2 t4);
      change with
-      (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4)
-        (apply_morphism n Out (m2 t1) t2));
+      (relation_of_relation_class unit Out (apply_morphism n Out (m1 a2) b1)
+        (apply_morphism n Out (m2 a1) b));
      generalize in match H3; clear H3;
-     generalize in match t3; clear t3;
-     generalize in match t1; clear t1;
+     generalize in match a1; clear a1;
+     generalize in match a2; clear a2;
      generalize in match H1; clear H1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim a 0;
       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
         simplify in H3;
         change in H1 with
          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
-        simplify in H;
-        apply H;
-         [ apply H1;
-           assumption
-         | assumption
-         ]
      | intro v;
        elim v 0;
        [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
          simplify in H3;
          change in H1 with
           (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
-         simplify in H;
-         apply H;
-          [ apply H1;
-            assumption
-          | assumption
-          ]
        | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
          simplify in H3;
          change in H1 with
           (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
-         simplify in H;
-         apply H;
-          [ apply H1;
-            assumption
-          | assumption
-          ]       
        ]
      | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
        simplify in H3;
        change in H1 with
         (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
-       simplify in H;
-       apply H;
-        [ apply H1;
-          assumption
-        | assumption
-        ]
      | intro v;
        elim v 0;
         [ intros (T1 r m1 m2 H1 t1 t3 H3);
@@ -630,15 +735,7 @@ theorem apply_morphism_compatibility_Right2Left:
           simplify in H3;
           change in H1 with
            (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
-        ] ;
-        simplify in H;
-        apply H;
-         [1,3:
-           apply H1;
-           assumption
-         |2,4:
-           assumption
-         ]
+        ]
      | intros (T m1 m2 H1 t1 t3 H3);
        simplify in H3;
        change in H1 with
@@ -649,103 +746,198 @@ theorem apply_morphism_compatibility_Right2Left:
         [ apply H1 
         | assumption
         ]
-     ]
+     ] ;
+     simplify in H;
+     apply H;
+      [1,3,5,7,9,11:
+        apply H1;
+        assumption
+      |2,4,6,8,10,12:
+        assumption
+      ]
    ]
 qed.
 
-(*
-Theorem apply_morphism_compatibility_Left2Right:
- ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
-   (args1 args2: product_of_arguments In).
+theorem apply_morphism_compatibility_Left2Right:
+ ∀In,Out.∀m1,m2: function_type_of_morphism_signature In Out.
+  ∀args1,args2: product_of_arguments In.
      make_compatibility_goal_aux ? ? m1 m2 →
       relation_of_product_of_arguments Left2Right ? args1 args2 →
         directed_relation_of_relation_class Left2Right ?
          (apply_morphism ? ? m1 args1)
          (apply_morphism ? ? m2 args2).
-  induction In; intros.
-    simpl in m1. m2. args1. args2. H0 |- *.
-    destruct a; simpl in H; hnf in H0.
-          apply H; exact H0.
-          destruct v; simpl in H0; apply H; exact H0.
-          apply H; exact H0.
-          destruct v; simpl in H0; apply H; exact H0.
-          rewrite H0; apply H; exact H0.
-
-    simpl in m1. m2. args1. args2. H0 |- *.
-   destruct args1; destruct args2; simpl.
-   destruct H0.
-   simpl in H.
-   destruct a; simpl in H.
-     apply IHIn.
-       apply H; exact H0.
-       exact H1.
-     destruct v.
-       apply IHIn.
-         apply H; exact H0.
-         exact H1.
-       apply IHIn.
-         apply H; exact H0.       
-          exact H1.
-       apply IHIn.
-         apply H; exact H0.
-         exact H1.
-       apply IHIn.
-         destruct v; simpl in H. H0; apply H; exact H0. 
-          exact H1.
-    rewrite H0; apply IHIn.
-      apply H.
-      exact H1.
-Qed.
+  intro; 
+  elim In 0; simplify; intros;
+   [ change in H1 with
+      (directed_relation_of_argument_class
+        (get_rewrite_direction Left2Right a) a args1 args2);
+     generalize in match H1; clear H1;
+     generalize in match H; clear H;
+     generalize in match args2; clear args2;
+     generalize in match args1; clear args1;
+     generalize in match m2; clear m2;
+     generalize in match m1; clear m1;
+     elim a 0; simplify;
+      [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
+        apply H;
+        exact H1
+      | intros 8 (v T1 r Hr m1 m2 args1 args2);
+        cases v;
+        intros (H H1);
+        simplify in H1;
+        apply H;
+        exact H1
+      | intros;
+        apply H1;
+        exact H2
+      | intros 7 (v);
+        cases v;
+        intros (H H1);
+        simplify in H1;
+        apply H;
+        exact H1
+      | intros;
+        simplify in H1;
+        rewrite > H1;
+        apply H;
+        exact H1
+      ]
+   | change in m1 with
+      (carrier_of_relation_class variance a →
+        function_type_of_morphism_signature n Out);
+     change in m2 with
+      (carrier_of_relation_class variance a →
+        function_type_of_morphism_signature n Out);
+     change in args1 with
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
+     change in args2 with
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
+     generalize in match H2; clear H2;
+     elim args2 0; clear args2;
+     elim args1; clear args1;
+     simplify in H2; change in H2:(? ? %) with
+       (relation_of_product_of_arguments Left2Right n b b1); 
+     elim H2; clear H2;
+     change with
+      (relation_of_relation_class unit Out (apply_morphism n Out (m1 a1) b)
+        (apply_morphism n Out (m2 a2) b1));
+     generalize in match H3; clear H3;
+     generalize in match a2; clear a2;
+     generalize in match a1; clear a1;
+     generalize in match H1; clear H1;
+     generalize in match m2; clear m2;
+     generalize in match m1; clear m1;
+     elim a 0;
+      [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
+        change in H1 with
+         (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
+     | intro v;
+       elim v 0;
+       [ intros (T1 r Hr m1 m2 H1 t1 t3 H3);
+         simplify in H3;
+         change in H1 with
+          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
+       | intros (T1 r Hr m1 m2 H1 t1 t3 H3);
+         simplify in H3;
+         change in H1 with
+          (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
+       ]
+     | intros (T1 r Hs m1 m2 H1 t1 t3 H3);
+       simplify in H3;
+       change in H1 with
+        (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
+     | intro v;
+       elim v 0;
+        [ intros (T1 r m1 m2 H1 t1 t3 H3);
+          simplify in H3;
+          change in H1 with
+           (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
+        | intros (T1 r m1 m2 H1 t1 t3 H3);
+          simplify in H3;
+          change in H1 with
+           (∀x1,x2:T1.r x2 x1 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
+        ]
+     | intros (T m1 m2 H1 t1 t3 H3);
+       simplify in H3;
+       change in H1 with
+        (∀x:T. make_compatibility_goal_aux n Out (m1 x) (m2 x));
+       rewrite > H3;
+       simplify in H;
+       apply H;
+        [ apply H1 
+        | assumption
+        ]
+     ] ;
+     simplify in H;
+     apply H;
+      [1,3,5,7,9,11:
+        apply H1;
+        assumption
+      |2,4,6,8,10,12:
+        assumption
+      ]
+   ]
+qed.
 
 definition interp :
- ∀Hole dir Out dir'. carrier_of_relation_class Hole →
-  Morphism_Context Hole dir Out dir' → carrier_of_relation_class Out.
- intros Hole dir Out dir' H t.
- elim t using
-  (@Morphism_Context_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
-    (fun ? L fcl => product_of_arguments L));
-  intros.
-   exact (apply_morphism ? ? (Function m) X).
-   exact H.
-   exact c.
-   exact x.
-   simpl;
-     rewrite <-
-       (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
-     exact X.
-   split.
-     rewrite <-
+ ∀Hole,dir,Out,dir'. carrier_of_relation_class ? Hole →
+  Morphism_Context Hole dir Out dir' → carrier_of_relation_class ? Out.
+ intros (Hole dir Out dir' H t).
+ apply
+  (Morphism_Context_rect2 Hole dir (λS,xx,yy. carrier_of_relation_class ? S)
+    (λxx,L,fcl.product_of_arguments L));
+  intros;
+   [8: apply t
+   |7: skip
+   | exact (apply_morphism ? ? (Function ? ? m) p)
+   | exact H
+   | exact c
+   | exact x
+   | simplify;
+     rewrite <
        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
-       exact X.
-       exact X0.
+     exact c1
+   | simplify;split;
+      [ rewrite <
+         (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
+        exact c1
+      | exact p
+      ]
+   ]
 qed.
 
+
 (*CSC: interp and interp_relation_class_list should be mutually defined. since
    the proof term of each one contains the proof term of the other one. However
    I cannot do that interactively (I should write the Fix by hand) *)
 definition interp_relation_class_list :
- ∀Hole dir dir' (L: Arguments). carrier_of_relation_class Hole →
+ ∀Hole,dir,dir'.∀L: Arguments. carrier_of_relation_class ? Hole →
   Morphism_Context_List Hole dir dir' L → product_of_arguments L.
- intros Hole dir dir' L H t.
- elim t using
-  (@Morphism_Context_List_rect2 Hole dir (fun S ? ? => carrier_of_relation_class S)
-    (fun ? L fcl => product_of_arguments L));
- intros.
-   exact (apply_morphism ? ? (Function m) X).
-   exact H.
-   exact c.
-   exact x.
-   simpl;
-     rewrite <-
-       (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
-     exact X.
-   split.
-     rewrite <-
+ intros (Hole dir dir' L H t);
+ apply
+  (Morphism_Context_List_rect2 Hole dir (λS,xx,yy.carrier_of_relation_class ? S)
+    (λxx,L,fcl.product_of_arguments L));
+ intros;
+  [8: apply t
+  |7: skip
+  | exact (apply_morphism ? ? (Function ? ? m) p)
+  | exact H
+  | exact c
+  | exact x
+  | simplify;
+     rewrite <
        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
-       exact X.
-       exact X0.
+     exact c1
+  | simplify; split;
+     [ rewrite <
+        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
+       exact c1
+     | exact p
+     ]
+  ]
 qed.
 
+(*
 Theorem setoid_rewrite:
  ∀Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
   (E: Morphism_Context Hole dir Out dir').
@@ -825,39 +1017,39 @@ Qed.
 (* impl IS A MORPHISM *)
 
 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
-unfold impl; tauto.
+unfold impl; tautobatch.
 Qed.
 
 (* and IS A MORPHISM *)
 
 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
- tauto.
+ tautobatch.
 Qed.
 
 (* or IS A MORPHISM *)
 
 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
- tauto.
+ tautobatch.
 Qed.
 
 (* not IS A MORPHISM *)
 
 Add Morphism not with signature iff ==> iff as Not_Morphism.
- tauto.
+ tautobatch.
 Qed.
 
 (* THE SAME EXAMPLES ON impl *)
 
 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
 Qed.
 
 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
 Qed.
 
 Add Morphism not with signature impl -→ impl as Not_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
 Qed.
 
 *)