X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=c60b4d1edc7c610f2fa7fe9b38854ddeb8671084;hb=285c01590113e2506c8b229458f4c99d3c7fc6a1;hp=c440795ffc2a099ee041fbe8039bc5f20bf478f3;hpb=b396fcf2d604ed9b9952217539ff69e2f5fff3c5;p=helm.git

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index c440795ff..c60b4d1ed 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -107,8 +107,8 @@ definition make_compatibility_goal_aux:
  ∀In,Out.∀f,g:function_type_of_morphism_signature In Out.Prop.
  intros 2; 
  elim In (a); simplify in f f1;
- generalize in match f; clear f;
  generalize in match f1; clear f1;
+ 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;
@@ -228,7 +228,7 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation:
     unfold transitive in H;
     unfold symmetric in sym;
     intro;
-    auto
+    auto new
   ].
 qed.
 
@@ -246,37 +246,51 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation:
     intro;
     unfold transitive in H;
     unfold symmetric in sym;
-    auto.
+    auto depth=4.
   ]
 qed.
 
 definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
- ∀(A: Type)(Aeq: relation A)(trans: transitive ? Aeq).
-  let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
-  let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
-   (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
- intros.
- exists Aeq.
- unfold make_compatibility_goal; simpl; unfold impl; eauto.
+ ∀A: Type.∀Aeq: relation A.∀trans: transitive ? Aeq.
+  let ASetoidClass1 := AsymmetricAreflexive ? Contravariant ? Aeq in
+  let ASetoidClass2 := AsymmetricAreflexive ? Covariant ? Aeq in
+   (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
+ intros;
+ apply mk_Morphism_Theory;
+ [ simplify;
+   apply Aeq
+ | simplify;
+   intros;
+   whd;
+   intros;
+   auto
+ ].
 qed.
 
 definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
- ∀(A: Type)(Aeq: relation A)(refl: reflexive ? Aeq)(trans: transitive ? Aeq).
-  let ASetoidClass1 := AsymmetricReflexive Contravariant refl in
-  let ASetoidClass2 := AsymmetricReflexive Covariant refl in
-   (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
- intros.
- exists Aeq.
- unfold make_compatibility_goal; simpl; unfold impl; eauto.
+ ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀trans: transitive ? Aeq.
+  let ASetoidClass1 := AsymmetricReflexive ? Contravariant ? ? refl in
+  let ASetoidClass2 := AsymmetricReflexive ? Covariant ? ? refl in
+   (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
+ intros;
+ apply mk_Morphism_Theory;
+ [ simplify;
+   apply Aeq
+ | simplify;
+   intros;
+   whd;
+   intro;
+   auto
+ ].
 qed.
 
 (* iff AS A RELATION *)
 
-Add Relation Prop iff
+(*DA PORTARE:Add Relation Prop iff
  reflexivity proved by iff_refl
  symmetry proved by iff_sym
  transitivity proved by iff_trans
- as iff_relation.
+ as iff_relation.*)
 
 (* every predicate is  morphism from Leibniz+ to Iff_Relation_Class *)
 definition morphism_theory_of_predicate :
@@ -284,274 +298,526 @@ definition morphism_theory_of_predicate :
   let In' := list_of_Leibniz_of_list_of_types In in
    function_type_of_morphism_signature In' Iff_Relation_Class →
     Morphism_Theory In' Iff_Relation_Class.
-  intros.
-  exists X.
-  induction In;  unfold make_compatibility_goal; simpl.
-    intro; apply iff_refl.
-    intro; apply (IHIn (X x)).
+  intros;
+  apply mk_Morphism_Theory;
+  [ apply f
+  | generalize in match f; clear f;
+    unfold In'; clear In';
+    elim In;
+     [ reduce;
+       intro;
+       alias id "iff_refl" = "cic:/matita/logic/coimplication/iff_refl.con".
+       apply iff_refl
+     | simplify;
+       intro x;
+       apply (H (f1 x))
+     ]
+  ].
 qed.
 
 (* impl AS A RELATION *)
 
-Theorem impl_trans: transitive ? impl.
- hnf; unfold impl; tauto.
-Qed.
+theorem impl_trans: transitive ? impl.
+ whd;
+ unfold impl;
+ intros;
+ auto.
+qed.
 
-Add Relation Prop impl
+(*DA PORTARE: Add Relation Prop impl
  reflexivity proved by impl_refl
  transitivity proved by impl_trans
- as impl_relation.
+ as impl_relation.*)
 
 (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
 
 inductive rewrite_direction : Type :=
-   Left2Right
- | Right2Left.
-
-Implicit Type dir: rewrite_direction.
+   Left2Right: rewrite_direction
+ | Right2Left: rewrite_direction.
 
 definition variance_of_argument_class : Argument_Class → option variance.
- destruct 1.
- exact None.
- exact (Some v).
- exact None.
- exact (Some v).
- exact None.
+ intros;
+ elim a;
+  [ apply None
+  | apply (Some ? t)
+  | apply None
+  | apply (Some ? t)
+  | apply None
+  ]
 qed.
 
 definition opposite_direction :=
- fun dir =>
+ λdir.
    match dir with
-       Left2Right => Right2Left
-     | Right2Left => Left2Right
-   end.
+    [ Left2Right ⇒ Right2Left
+    | Right2Left ⇒ Left2Right
+    ].
 
-Lemma opposite_direction_idempotent:
- ∀dir. (opposite_direction (opposite_direction dir)) = dir.
-  destruct dir; reflexivity.
-Qed.
+lemma opposite_direction_idempotent:
+ ∀dir. opposite_direction (opposite_direction dir) = dir.
+  intros;
+  elim dir;
+  reflexivity.
+qed.
 
 inductive check_if_variance_is_respected :
  option variance → rewrite_direction → rewrite_direction →  Prop
 :=
-   MSNone : ∀dir dir'. check_if_variance_is_respected None dir dir'
- | MSCovariant : ∀dir. check_if_variance_is_respected (Some Covariant) dir dir
+   MSNone : ∀dir,dir'. check_if_variance_is_respected (None ?) dir dir'
+ | MSCovariant : ∀dir. check_if_variance_is_respected (Some ? Covariant) dir dir
  | MSContravariant :
      ∀dir.
-      check_if_variance_is_respected (Some Contravariant) dir (opposite_direction dir).
+      check_if_variance_is_respected (Some ? Contravariant) dir (opposite_direction dir).
 
 definition relation_class_of_reflexive_relation_class:
  Reflexive_Relation_Class → Relation_Class.
- induction 1.
-   exact (SymmetricReflexive ? s r).
-   exact (AsymmetricReflexive tt r).
-   exact (Leibniz ? T).
+ intro;
+ elim r;
+  [ apply (SymmetricReflexive ? ? ? H H1)
+  | apply (AsymmetricReflexive ? something ? ? H)
+  | apply (Leibniz ? T)
+  ]
 qed.
 
 definition relation_class_of_areflexive_relation_class:
  Areflexive_Relation_Class → Relation_Class.
- induction 1.
-   exact (SymmetricAreflexive ? s).
-   exact (AsymmetricAreflexive tt Aeq).
+ intro;
+ elim a;
+  [ apply (SymmetricAreflexive ? ? ? H)
+  | apply (AsymmetricAreflexive ? something ? r)
+  ]
 qed.
 
 definition carrier_of_reflexive_relation_class :=
- fun R => carrier_of_relation_class (relation_class_of_reflexive_relation_class R).
+ λR.carrier_of_relation_class ? (relation_class_of_reflexive_relation_class R).
 
 definition carrier_of_areflexive_relation_class :=
- fun R => carrier_of_relation_class (relation_class_of_areflexive_relation_class R).
+ λR.carrier_of_relation_class ? (relation_class_of_areflexive_relation_class R).
 
 definition relation_of_areflexive_relation_class :=
- fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R).
+ λR.relation_of_relation_class ? (relation_class_of_areflexive_relation_class R).
 
-inductive Morphism_Context Hole dir : Relation_Class → rewrite_direction →  Type :=
+inductive Morphism_Context (Hole: Relation_Class) (dir:rewrite_direction) : Relation_Class → rewrite_direction →  Type :=
     App :
-      ∀In Out dir'.
+      ∀In,Out,dir'.
         Morphism_Theory In Out → Morphism_Context_List Hole dir dir' In →
            Morphism_Context Hole dir Out dir'
   | ToReplace : Morphism_Context Hole dir Hole dir
   | ToKeep :
-     ∀S dir'.
+     ∀S,dir'.
       carrier_of_reflexive_relation_class S →
         Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
  | ProperElementToKeep :
-     ∀S dir' (x: carrier_of_areflexive_relation_class S).
+     ∀S,dir'.∀x: carrier_of_areflexive_relation_class S.
       relation_of_areflexive_relation_class S x x →
         Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir'
-with Morphism_Context_List Hole dir :
+with Morphism_Context_List :
    rewrite_direction → Arguments → Type
 :=
     fcl_singl :
-      ∀S dir' dir''.
+      ∀S,dir',dir''.
        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
-         Morphism_Context_List Hole dir dir'' (singl S)
+         Morphism_Context_List Hole dir dir'' (singl ? S)
  | fcl_cons :
-      ∀S L dir' dir''.
+      ∀S,L,dir',dir''.
        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' →
         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' →
          Morphism_Context_List Hole dir dir'' L →
-          Morphism_Context_List Hole dir dir'' (cons S L).
-
-Scheme Morphism_Context_rect2 := Induction for Morphism_Context  Sort Type
-with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type.
+          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.
 
 definition product_of_arguments : Arguments → Type.
- induction 1.
-   exact (carrier_of_relation_class a).
-   exact (prod (carrier_of_relation_class a) IHX).
+ intro;
+ elim a;
+  [ apply (carrier_of_relation_class ? t)
+  | apply (Prod (carrier_of_relation_class ? t) T)
+  ]
 qed.
 
 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
- intros dir R.
-destruct (variance_of_argument_class R).
-   destruct v.
-     exact dir.                                      (* covariant *)
-     exact (opposite_direction dir). (* contravariant *)
-   exact dir.                                       (* symmetric relation *)
+ intros (dir R);
+ cases (variance_of_argument_class R);
+  [ exact dir
+  | cases a;
+     [ exact dir                      (* covariant *)
+     | exact (opposite_direction dir) (* contravariant *)
+     ]
+  ]
 qed.
 
 definition directed_relation_of_relation_class:
- ∀dir (R: Relation_Class).
-   carrier_of_relation_class R → carrier_of_relation_class R → Prop.
- destruct 1.
-   exact (@relation_of_relation_class unit).
-   intros; exact (relation_of_relation_class ? X0 X).
+ ∀dir:rewrite_direction.∀R: Relation_Class.
+   carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
+ intros;
+ cases r;
+  [ exact (relation_of_relation_class ? ? c c1)
+  | apply (relation_of_relation_class ? ? c1 c)
+  ]
 qed.
 
 definition directed_relation_of_argument_class:
- ∀dir (R: Argument_Class).
-   carrier_of_relation_class R → carrier_of_relation_class R → Prop.
-  intros dir R.
-  rewrite <-
-   (about_carrier_of_relation_class_and_relation_class_of_argument_class R).
-  exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)).
+ ∀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
+   ]
 qed.
 
-
 definition relation_of_product_of_arguments:
- ∀dir In.
+ ∀dir:rewrite_direction.∀In.
   product_of_arguments In → product_of_arguments In → Prop.
- induction In.
-   simpl.
-   exact (directed_relation_of_argument_class (get_rewrite_direction dir a) a).
-
-   simpl; intros.
-   destruct X; destruct X0.
-   apply and.
-     exact
-      (directed_relation_of_argument_class (get_rewrite_direction dir a) a c c0).
-     exact (IHIn p p0).
+ intros 2;
+ elim In 0;
+  [ simplify;
+    intro;
+    exact (directed_relation_of_argument_class (get_rewrite_direction r t) t)
+  | 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;
+   apply And;
+    [ exact
+      (directed_relation_of_argument_class (get_rewrite_direction r t) t a a1)
+    | exact (R b b1)
+    ]
+  ]
 qed. 
 
 definition apply_morphism:
- ∀In Out (m: function_type_of_morphism_signature In Out)
-  (args: product_of_arguments In). carrier_of_relation_class Out.
- intros.
- induction In.
-   exact (m args).
-   simpl in m. args.
-   destruct args.
-   exact (IHIn (m c) p).
+ ∀In,Out.∀m: function_type_of_morphism_signature In Out.
+  ∀args: product_of_arguments In. carrier_of_relation_class ? Out.
+ intro;
+ elim In;
+  [ exact (f p)
+  | change in p with (Prod (carrier_of_relation_class variance t) (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)
+  ]
 qed.
 
-Theorem apply_morphism_compatibility_Right2Left:
- ∀In Out (m1 m2: function_type_of_morphism_signature In Out)
-   (args1 args2: product_of_arguments In).
+theorem apply_morphism_compatibility_Right2Left:
+ ∀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 Right2Left ? args1 args2 →
         directed_relation_of_relation_class Right2Left ?
          (apply_morphism ? ? m2 args1)
          (apply_morphism ? ? m1 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.
-     destruct v.
-       apply IHIn.
-         apply H; exact H0.
-         exact H1.
-       apply IHIn.
-         apply H; exact H0.       
-          exact H1.
-    rewrite H0; apply IHIn.
-      apply H.
-      exact H1.
-Qed.
+  intro;
+  elim In;
+   [ simplify in m1 m2 args1 args2 ⊢ %;
+     change in H1 with
+      (directed_relation_of_argument_class
+        (get_rewrite_direction Right2Left t) t 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;
+      [ 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;
+        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 t →
+        function_type_of_morphism_signature n Out);
+     change in m2 with
+      (carrier_of_relation_class variance t →
+        function_type_of_morphism_signature n Out);
+     change in args1 with
+      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+     change in args2 with
+      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+     generalize in match H2; clear H2;
+     elim args2 0; clear args2;
+     elim args1; clear args1;
+     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));
+     generalize in match H3; clear H3;
+     generalize in match t3; clear t3;
+     generalize in match t1; clear t1;
+     generalize in match H1; clear H1;
+     generalize in match m2; clear m2;
+     generalize in match m1; clear m1;
+     elim t 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));
+     | 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.
 
-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;
+   [ simplify in m1 m2 args1 args2 ⊢ %;
+     change in H1 with
+      (directed_relation_of_argument_class
+        (get_rewrite_direction Left2Right t) t 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;
+      [ 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;
+        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 t →
+        function_type_of_morphism_signature n Out);
+     change in m2 with
+      (carrier_of_relation_class variance t →
+        function_type_of_morphism_signature n Out);
+     change in args1 with
+      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+     change in args2 with
+      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+     generalize in match H2; clear H2;
+     elim args2 0; clear args2;
+     elim args1; clear args1;
+     elim H2; clear H2;
+     change in H4 with
+      (relation_of_product_of_arguments Left2Right n t2 t4);
+     change with
+      (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2)
+        (apply_morphism n Out (m2 t3) t4));
+     generalize in match H3; clear H3;
+     generalize in match t3; clear t3;
+     generalize in match t1; clear t1;
+     generalize in match H1; clear H1;
+     generalize in match m2; clear m2;
+     generalize in match m1; clear m1;
+     elim t 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));
+     | 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));
+ ∀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.
    exact (apply_morphism ? ? (Function m) X).
    exact H.
@@ -668,15 +934,6 @@ Theorem setoid_rewrite:
      exact H1.
 Qed.
 
-(* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *)
-
-record Setoid_Theory  (A: Type) (Aeq: relation A) : Prop := 
-  {Seq_refl : ∀x:A. Aeq x x;
-   Seq_sym : ∀x y:A. Aeq x y → Aeq y x;
-   Seq_trans : ∀x y z:A. Aeq x y → Aeq y z → Aeq x z}.
-
-(* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
-
 (* A FEW EXAMPLES ON iff *)
 
 (* impl IS A MORPHISM *)
@@ -717,31 +974,4 @@ Add Morphism not with signature impl -→ impl as Not_Morphism2.
  unfold impl; tauto.
 Qed.
 
-(* FOR BACKWARD COMPATIBILITY *)
-Implicit Arguments Setoid_Theory [].
-Implicit Arguments Seq_refl [].
-Implicit Arguments Seq_sym [].
-Implicit Arguments Seq_trans [].
-
-
-(* Some tactics for manipulating Setoid Theory not officially 
-   declared as Setoid. *)
-
-Ltac trans_st x := match goal with 
-  | H : Setoid_Theory ? ?eqA |- ?eqA ? ? => 
-     apply (Seq_trans ? ? H) with x; auto
- end.
-
-Ltac sym_st := match goal with 
-  | H : Setoid_Theory ? ?eqA |- ?eqA ? ? => 
-     apply (Seq_sym ? ? H); auto
- end.
-
-Ltac refl_st := match goal with 
-  | H : Setoid_Theory ? ?eqA |- ?eqA ? ? => 
-     apply (Seq_refl ? ? H); auto
- end.
-
-definition gen_st : ∀A : Set. Setoid_Theory ? (@eq A).
-Proof. constructor; congruence. Qed.
-
+*)