Découpage de Setoid.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10147 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 678 insertions, 653 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 508a0231e..da999dfe7 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -9,660 +9,10 @@
 
 (*i $Id$: i*)
 
-Require Export Relation_Definitions.
+Require Export Setoid_tac.
+Require Export Setoid_Prop.
 
-Set Implicit Arguments.
-
-(** * Definitions of [Relation_Class] and n-ary [Morphism_Theory] *)
-
-(* X will be used to distinguish covariant arguments whose type is an   *)
-(* Asymmetric* relation from contravariant arguments of the same type *)
-Inductive X_Relation_Class (X: Type) : Type :=
-   SymmetricReflexive :
-     forall A Aeq, symmetric A Aeq -> reflexive _ Aeq -> X_Relation_Class X
- | AsymmetricReflexive : X -> forall A Aeq, reflexive A Aeq -> X_Relation_Class X
- | SymmetricAreflexive : forall A Aeq, symmetric A Aeq -> X_Relation_Class X
- | AsymmetricAreflexive : X -> forall A (Aeq : relation A), X_Relation_Class X
- | Leibniz : Type -> X_Relation_Class X.
-
-Inductive variance : Set :=
-   Covariant
- | Contravariant.
-
-Definition Argument_Class := X_Relation_Class variance.
-Definition Relation_Class := X_Relation_Class unit.
-
-Inductive Reflexive_Relation_Class : Type :=
-   RSymmetric :
-     forall A Aeq, symmetric A Aeq -> reflexive _ Aeq -> Reflexive_Relation_Class
- | RAsymmetric :
-     forall A Aeq, reflexive A Aeq -> Reflexive_Relation_Class
- | RLeibniz : Type -> Reflexive_Relation_Class.
-
-Inductive Areflexive_Relation_Class  : Type :=
- | ASymmetric : forall A Aeq, symmetric A Aeq -> Areflexive_Relation_Class
- | AAsymmetric : forall A (Aeq : relation A), Areflexive_Relation_Class.
-
-Implicit Type Hole Out: Relation_Class.
-
-Definition relation_class_of_argument_class : Argument_Class -> Relation_Class.
-  destruct 1.
-  exact (SymmetricReflexive _ s r).
-  exact (AsymmetricReflexive tt r).
-  exact (SymmetricAreflexive _ s).
-  exact (AsymmetricAreflexive tt Aeq).
-  exact (Leibniz _ T).
-Defined.
-
-Definition carrier_of_relation_class : forall X, X_Relation_Class X -> Type.
-  destruct 1.
-  exact A.
-  exact A.
-  exact A.
-  exact A.
-  exact T.
-Defined.
-
-Definition relation_of_relation_class :
-  forall X R, @carrier_of_relation_class X R -> carrier_of_relation_class R -> Prop.
-  destruct R.
-  exact Aeq.
-  exact Aeq.
-  exact Aeq.
-  exact Aeq.
-  exact (@eq T).
-Defined.
-
-Lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
-  forall R,
-    carrier_of_relation_class (relation_class_of_argument_class R) =
-    carrier_of_relation_class R.
-  destruct R; reflexivity.
-Defined.
-
-Inductive nelistT (A : Type) : Type :=
-   singl : A -> nelistT A
- | necons : A -> nelistT A -> nelistT A.
-
-Definition Arguments := nelistT Argument_Class.
-
-Implicit Type In: Arguments.
-
-Definition function_type_of_morphism_signature :
-  Arguments -> Relation_Class -> Type.
-  intros In Out.
-  induction In.
-    exact (carrier_of_relation_class a -> carrier_of_relation_class Out).
-    exact (carrier_of_relation_class a -> IHIn).
-Defined. 
-
-Definition make_compatibility_goal_aux:
-  forall In Out
-    (f g: function_type_of_morphism_signature In Out), Prop.
-  intros; induction In; simpl in f, g.
-    induction a; simpl in f, g.
-      exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
-      destruct x.
-        exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
-        exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f x1) (g x2)).
-      exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
-      destruct x.
-        exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
-        exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f x1) (g x2)).
-      exact (forall x, relation_of_relation_class Out (f x) (g x)).
-  induction a; simpl in f, g.
-    exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
-    destruct x.
-      exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
-      exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
-    exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
-    destruct x.
-      exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
-      exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
-    exact (forall x, IHIn (f x) (g x)).
-Defined. 
-
-Definition make_compatibility_goal :=
-  (fun In Out f => make_compatibility_goal_aux In Out f f).
-
-Record Morphism_Theory In Out : Type :=
-  { Function : function_type_of_morphism_signature In Out;
-    Compat : make_compatibility_goal In Out Function }.
-
-(** The [iff] relation class *)
-
-Definition Iff_Relation_Class : Relation_Class.
-  eapply (@SymmetricReflexive unit _ iff).
-  exact iff_sym.
-  exact iff_refl.
-Defined.
-
-(** The [impl] relation class *)
-
-Definition impl (A B: Prop) := A -> B.
-
-Theorem impl_refl: reflexive _ impl.
-Proof.
-  hnf; unfold impl; tauto.
-Qed.
-
-Definition Impl_Relation_Class : Relation_Class.
-  eapply (@AsymmetricReflexive unit tt _ impl).
-  exact impl_refl.
-Defined.
-
-(** Every function is a morphism from Leibniz+ to Leibniz *)
-
-Definition list_of_Leibniz_of_list_of_types: nelistT Type -> Arguments.
- induction 1.
-   exact (singl (Leibniz _ a)).
-   exact (necons (Leibniz _ a) IHX).
-Defined.
-
-Definition morphism_theory_of_function :
-  forall (In: nelistT Type) (Out: Type),
-    let In' := list_of_Leibniz_of_list_of_types In in
-      let Out' := Leibniz _ Out in
-	function_type_of_morphism_signature In' Out' ->
-	Morphism_Theory In' Out'.
-  intros.
-  exists X.
-  induction In;  unfold make_compatibility_goal; simpl.
-    reflexivity.
-    intro; apply (IHIn (X x)).
-Defined.
-
-(** Every predicate is a morphism from Leibniz+ to Iff_Relation_Class *)
-
-Definition morphism_theory_of_predicate :
-  forall (In: nelistT Type),
-    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)).
-Defined.
-
-(** * Utility functions to prove that every transitive relation is a morphism *)
-
-Definition equality_morphism_of_symmetric_areflexive_transitive_relation:
- forall (A: Type)(Aeq: relation A)(sym: symmetric _ Aeq)(trans: transitive _ Aeq),
-  let ASetoidClass := SymmetricAreflexive _ sym in
-   (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
- intros.
- exists Aeq.
- unfold make_compatibility_goal; simpl; split; eauto.
-Defined.
-
-Definition equality_morphism_of_symmetric_reflexive_transitive_relation:
- forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(sym: symmetric _ Aeq)
-  (trans: transitive _ Aeq), let ASetoidClass := SymmetricReflexive _ sym refl in
-   (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
- intros.
- exists Aeq.
- unfold make_compatibility_goal; simpl; split; eauto.
-Defined.
-
-Definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
- forall (A: Type)(Aeq: relation A)(trans: transitive _ Aeq),
-  let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
-  let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
-   (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
- intros.
- exists Aeq.
- unfold make_compatibility_goal; simpl; unfold impl; eauto.
-Defined.
-
-Definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
- forall (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 (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
- intros.
- exists Aeq.
- unfold make_compatibility_goal; simpl; unfold impl; eauto.
-Defined.
-
-(** * A few examples on [iff] *)
-
-(** [iff] as a relation *)
-
-Add Relation Prop iff
-  reflexivity proved by iff_refl
-  symmetry proved by iff_sym
-  transitivity proved by iff_trans
-as iff_relation.
-
-(** [impl] as a relation *)
-
-Theorem impl_trans: transitive _ impl.
-Proof.
-  hnf; unfold impl; tauto.
-Qed.
-
-Add Relation Prop impl
-  reflexivity proved by impl_refl
-  transitivity proved by impl_trans
-as impl_relation.
-
-(** [impl] is a morphism *)
-
-Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
-Proof.
-  unfold impl; tauto.
-Qed.
-
-(** [and] is a morphism *)
-
-Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
- tauto.
-Qed.
-
-(** [or] is a morphism *)
-
-Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
-Proof.
-  tauto.
-Qed.
-
-(** [not] is a morphism *)
-
-Add Morphism not with signature iff ==> iff as Not_Morphism.
-Proof.
-  tauto.
-Qed.
-
-(** The same examples on [impl] *)
-
-Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
-Proof.
-  unfold impl; tauto.
-Qed.
-
-Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
-Proof.
-  unfold impl; tauto.
-Qed.
-
-Add Morphism not with signature impl --> impl as Not_Morphism2.
-Proof.
-  unfold impl; tauto.
-Qed.
-
-(** * The CIC part of the reflexive tactic ([setoid_rewrite]) *)
-
-Inductive rewrite_direction : Type :=
-  | Left2Right
-  | Right2Left.
-
-Implicit Type dir: 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.
-Defined.
-
-Definition opposite_direction :=
-  fun dir =>
-    match dir with
-      | Left2Right => Right2Left
-      | Right2Left => Left2Right
-   end.
-
-Lemma opposite_direction_idempotent:
-  forall dir, (opposite_direction (opposite_direction dir)) = dir.
-Proof.
-  destruct dir; reflexivity.
-Qed.
-
-Inductive check_if_variance_is_respected :
-  option variance -> rewrite_direction -> rewrite_direction ->  Prop :=
-  | MSNone : forall dir dir', check_if_variance_is_respected None dir dir'
-  | MSCovariant : forall dir, check_if_variance_is_respected (Some Covariant) dir dir
-  | MSContravariant :
-    forall 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).
-Defined.
-
-Definition relation_class_of_areflexive_relation_class:
-  Areflexive_Relation_Class -> Relation_Class.
-  induction 1.
-    exact (SymmetricAreflexive _ s).
-    exact (AsymmetricAreflexive tt Aeq).
-Defined.
-
-Definition carrier_of_reflexive_relation_class :=
-  fun 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).
-
-Definition relation_of_areflexive_relation_class :=
-  fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R).
-
-Inductive Morphism_Context Hole dir : Relation_Class -> rewrite_direction ->  Type :=
-  | App :
-    forall 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 :
-    forall S dir',
-      carrier_of_reflexive_relation_class S ->
-      Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
-  | ProperElementToKeep :
-    forall 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 :
-   rewrite_direction -> Arguments -> Type
-:=
-    fcl_singl :
-      forall 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)
- | fcl_cons :
-      forall 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'' (necons S L).
-
-Scheme Morphism_Context_rect2 := Induction for Morphism_Context  Sort Type
-with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type.
-
-Definition product_of_arguments : Arguments -> Type.
-  induction 1.
-  exact (carrier_of_relation_class a).
-  exact (prod (carrier_of_relation_class a) IHX).
-Defined.
-
-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 *)
-Defined.
-
-Definition directed_relation_of_relation_class:
-  forall 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).
-Defined.
-
-Definition directed_relation_of_argument_class:
-  forall 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)).
-Defined.
-
-
-Definition relation_of_product_of_arguments:
-  forall dir 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).
-Defined. 
-
-Definition apply_morphism:
-  forall 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).
-Defined.
-
-Theorem apply_morphism_compatibility_Right2Left:
-  forall 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.
-
-Theorem apply_morphism_compatibility_Left2Right:
-  forall 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).
-Proof.
-  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.
-
-Definition interp :
- forall 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 <-
-       (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
-       exact X.
-       exact X0.
-Defined.
-
-(* 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 :
-  forall 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 <-
-    (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
-    exact X.
-  exact X0.
-Defined.
-
-Theorem setoid_rewrite:
-  forall Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
-    (E: Morphism_Context Hole dir Out dir'),
-    (directed_relation_of_relation_class dir Hole E1 E2) ->
-    (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
-Proof.
-  intros.
-  elim E using
-    (@Morphism_Context_rect2 Hole dir
-      (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
-      (fun dir'' L fcl =>
-        relation_of_product_of_arguments dir'' _
-        (interp_relation_class_list E1 fcl)
-        (interp_relation_class_list E2 fcl))); intros.
-  change (directed_relation_of_relation_class dir'0 Out0
-    (apply_morphism _ _ (Function m) (interp_relation_class_list E1 m0))
-    (apply_morphism _ _ (Function m) (interp_relation_class_list E2 m0))).
-  destruct dir'0.
-    apply apply_morphism_compatibility_Left2Right.
-      exact (Compat m).
-      exact H0.
-    apply apply_morphism_compatibility_Right2Left.
-      exact (Compat m).
-      exact H0.
-
-  exact H.
-
-  unfold interp, Morphism_Context_rect2.
-  (* CSC: reflexivity used here *)
-  destruct S; destruct dir'0; simpl; (apply r || reflexivity).
-  
-  destruct dir'0; exact r.
-
-  destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
-    unfold get_rewrite_direction; simpl.
-  destruct dir'0; destruct dir'';
-    (exact H0 ||
-      unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
-  (* the following mess with generalize/clear/intros is to help Coq resolving *)
-  (* second order unification problems.                                       *)
-  generalize m c H0; clear H0 m c; inversion c;
-    generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
-      (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
-  destruct dir'0; destruct dir'';
-    (exact H0 ||
-      unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
-  (* the following mess with generalize/clear/intros is to help Coq resolving *)
-  (* second order unification problems.                                       *)
-  generalize m c H0; clear H0 m c; inversion c;
-    generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
-      (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
-  destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
-
-  change
-    (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
-       (eq_rect _ (fun T : Type => T) (interp E1 m) _
-         (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
-       (eq_rect _ (fun T : Type => T) (interp E2 m) _
-         (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
-       relation_of_product_of_arguments dir'' _
-       (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
-  split.
-  clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
-    destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
-      inversion c.
-        rewrite <- H3; exact H0.
-        rewrite (opposite_direction_idempotent dir'0); exact H0.
-      destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
-      inversion c.
-        rewrite <- H3; exact H0.
-        rewrite (opposite_direction_idempotent dir'0); exact H0.
-      destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
-    exact H1.
-  Qed.
-
-(** * Miscelenous *)
-
-(** For backwark compatibility *)
+(** For backward compatibility *)
 
 Record Setoid_Theory  (A: Type) (Aeq: relation A) : Prop := 
   { Seq_refl : forall x:A, Aeq x x;
diff --git a/theories/Setoids/Setoid_Prop.v b/theories/Setoids/Setoid_Prop.v
new file mode 100644
index 000000000..9c0b4b2b6
--- /dev/null
+++ b/theories/Setoids/Setoid_Prop.v
@@ -0,0 +1,79 @@
+
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$: i*)
+
+Require Import Setoid_tac.
+
+(** * A few examples on [iff] *)
+
+(** [iff] as a relation *)
+
+Add Relation Prop iff
+  reflexivity proved by iff_refl
+  symmetry proved by iff_sym
+  transitivity proved by iff_trans
+as iff_relation.
+
+(** [impl] as a relation *)
+
+Theorem impl_trans: transitive _ impl.
+Proof.
+  hnf; unfold impl; tauto.
+Qed.
+
+Add Relation Prop impl
+  reflexivity proved by impl_refl
+  transitivity proved by impl_trans
+as impl_relation.
+
+(** [impl] is a morphism *)
+
+Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
+Proof.
+  unfold impl; tauto.
+Qed.
+
+(** [and] is a morphism *)
+
+Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
+ tauto.
+Qed.
+
+(** [or] is a morphism *)
+
+Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
+Proof.
+  tauto.
+Qed.
+
+(** [not] is a morphism *)
+
+Add Morphism not with signature iff ==> iff as Not_Morphism.
+Proof.
+  tauto.
+Qed.
+
+(** The same examples on [impl] *)
+
+Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
+Proof.
+  unfold impl; tauto.
+Qed.
+
+Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
+Proof.
+  unfold impl; tauto.
+Qed.
+
+Add Morphism not with signature impl --> impl as Not_Morphism2.
+Proof.
+  unfold impl; tauto.
+Qed.
+
diff --git a/theories/Setoids/Setoid_tac.v b/theories/Setoids/Setoid_tac.v
new file mode 100644
index 000000000..f979ec11c
--- /dev/null
+++ b/theories/Setoids/Setoid_tac.v
@@ -0,0 +1,596 @@
+
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Relation_Definitions.
+
+Set Implicit Arguments.
+
+(** * Definitions of [Relation_Class] and n-ary [Morphism_Theory] *)
+
+(* X will be used to distinguish covariant arguments whose type is an   *)
+(* Asymmetric* relation from contravariant arguments of the same type *)
+Inductive X_Relation_Class (X: Type) : Type :=
+   SymmetricReflexive :
+     forall A Aeq, symmetric A Aeq -> reflexive _ Aeq -> X_Relation_Class X
+ | AsymmetricReflexive : X -> forall A Aeq, reflexive A Aeq -> X_Relation_Class X
+ | SymmetricAreflexive : forall A Aeq, symmetric A Aeq -> X_Relation_Class X
+ | AsymmetricAreflexive : X -> forall A (Aeq : relation A), X_Relation_Class X
+ | Leibniz : Type -> X_Relation_Class X.
+
+Inductive variance : Set :=
+   Covariant
+ | Contravariant.
+
+Definition Argument_Class := X_Relation_Class variance.
+Definition Relation_Class := X_Relation_Class unit.
+
+Inductive Reflexive_Relation_Class : Type :=
+   RSymmetric :
+     forall A Aeq, symmetric A Aeq -> reflexive _ Aeq -> Reflexive_Relation_Class
+ | RAsymmetric :
+     forall A Aeq, reflexive A Aeq -> Reflexive_Relation_Class
+ | RLeibniz : Type -> Reflexive_Relation_Class.
+
+Inductive Areflexive_Relation_Class  : Type :=
+ | ASymmetric : forall A Aeq, symmetric A Aeq -> Areflexive_Relation_Class
+ | AAsymmetric : forall A (Aeq : relation A), Areflexive_Relation_Class.
+
+Implicit Type Hole Out: Relation_Class.
+
+Definition relation_class_of_argument_class : Argument_Class -> Relation_Class.
+  destruct 1.
+  exact (SymmetricReflexive _ s r).
+  exact (AsymmetricReflexive tt r).
+  exact (SymmetricAreflexive _ s).
+  exact (AsymmetricAreflexive tt Aeq).
+  exact (Leibniz _ T).
+Defined.
+
+Definition carrier_of_relation_class : forall X, X_Relation_Class X -> Type.
+  destruct 1.
+  exact A.
+  exact A.
+  exact A.
+  exact A.
+  exact T.
+Defined.
+
+Definition relation_of_relation_class :
+  forall X R, @carrier_of_relation_class X R -> carrier_of_relation_class R -> Prop.
+  destruct R.
+  exact Aeq.
+  exact Aeq.
+  exact Aeq.
+  exact Aeq.
+  exact (@eq T).
+Defined.
+
+Lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
+  forall R,
+    carrier_of_relation_class (relation_class_of_argument_class R) =
+    carrier_of_relation_class R.
+  destruct R; reflexivity.
+Defined.
+
+Inductive nelistT (A : Type) : Type :=
+   singl : A -> nelistT A
+ | necons : A -> nelistT A -> nelistT A.
+
+Definition Arguments := nelistT Argument_Class.
+
+Implicit Type In: Arguments.
+
+Definition function_type_of_morphism_signature :
+  Arguments -> Relation_Class -> Type.
+  intros In Out.
+  induction In.
+    exact (carrier_of_relation_class a -> carrier_of_relation_class Out).
+    exact (carrier_of_relation_class a -> IHIn).
+Defined. 
+
+Definition make_compatibility_goal_aux:
+  forall In Out
+    (f g: function_type_of_morphism_signature In Out), Prop.
+  intros; induction In; simpl in f, g.
+    induction a; simpl in f, g.
+      exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
+      destruct x.
+        exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
+        exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f x1) (g x2)).
+      exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
+      destruct x.
+        exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)).
+        exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f x1) (g x2)).
+      exact (forall x, relation_of_relation_class Out (f x) (g x)).
+  induction a; simpl in f, g.
+    exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
+    destruct x.
+      exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
+      exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
+    exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
+    destruct x.
+      exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
+      exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
+    exact (forall x, IHIn (f x) (g x)).
+Defined. 
+
+Definition make_compatibility_goal :=
+  (fun In Out f => make_compatibility_goal_aux In Out f f).
+
+Record Morphism_Theory In Out : Type :=
+  { Function : function_type_of_morphism_signature In Out;
+    Compat : make_compatibility_goal In Out Function }.
+
+
+(** The [iff] relation class *)
+
+Definition Iff_Relation_Class : Relation_Class.
+  eapply (@SymmetricReflexive unit _ iff).
+  exact iff_sym.
+  exact iff_refl.
+Defined.
+
+(** The [impl] relation class *)
+
+Definition impl (A B: Prop) := A -> B.
+
+Theorem impl_refl: reflexive _ impl.
+Proof.
+  hnf; unfold impl; tauto.
+Qed.
+
+Definition Impl_Relation_Class : Relation_Class.
+  eapply (@AsymmetricReflexive unit tt _ impl).
+  exact impl_refl.
+Defined.
+
+(** Every function is a morphism from Leibniz+ to Leibniz *)
+
+Definition list_of_Leibniz_of_list_of_types: nelistT Type -> Arguments.
+ induction 1.
+   exact (singl (Leibniz _ a)).
+   exact (necons (Leibniz _ a) IHX).
+Defined.
+
+Definition morphism_theory_of_function :
+  forall (In: nelistT Type) (Out: Type),
+    let In' := list_of_Leibniz_of_list_of_types In in
+      let Out' := Leibniz _ Out in
+	function_type_of_morphism_signature In' Out' ->
+	Morphism_Theory In' Out'.
+  intros.
+  exists X.
+  induction In;  unfold make_compatibility_goal; simpl.
+    reflexivity.
+    intro; apply (IHIn (X x)).
+Defined.
+
+(** Every predicate is a morphism from Leibniz+ to Iff_Relation_Class *)
+
+Definition morphism_theory_of_predicate :
+  forall (In: nelistT Type),
+    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)).
+Defined.
+
+(** * Utility functions to prove that every transitive relation is a morphism *)
+
+Definition equality_morphism_of_symmetric_areflexive_transitive_relation:
+ forall (A: Type)(Aeq: relation A)(sym: symmetric _ Aeq)(trans: transitive _ Aeq),
+  let ASetoidClass := SymmetricAreflexive _ sym in
+   (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
+ intros.
+ exists Aeq.
+ unfold make_compatibility_goal; simpl; split; eauto.
+Defined.
+
+Definition equality_morphism_of_symmetric_reflexive_transitive_relation:
+ forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(sym: symmetric _ Aeq)
+  (trans: transitive _ Aeq), let ASetoidClass := SymmetricReflexive _ sym refl in
+   (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
+ intros.
+ exists Aeq.
+ unfold make_compatibility_goal; simpl; split; eauto.
+Defined.
+
+Definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
+ forall (A: Type)(Aeq: relation A)(trans: transitive _ Aeq),
+  let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
+  let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
+   (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
+ intros.
+ exists Aeq.
+ unfold make_compatibility_goal; simpl; unfold impl; eauto.
+Defined.
+
+Definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
+ forall (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 (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
+ intros.
+ exists Aeq.
+ unfold make_compatibility_goal; simpl; unfold impl; eauto.
+Defined.
+
+(** * The CIC part of the reflexive tactic ([setoid_rewrite]) *)
+
+Inductive rewrite_direction : Type :=
+  | Left2Right
+  | Right2Left.
+
+Implicit Type dir: 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.
+Defined.
+
+Definition opposite_direction :=
+  fun dir =>
+    match dir with
+      | Left2Right => Right2Left
+      | Right2Left => Left2Right
+   end.
+
+Lemma opposite_direction_idempotent:
+  forall dir, (opposite_direction (opposite_direction dir)) = dir.
+Proof.
+  destruct dir; reflexivity.
+Qed.
+
+Inductive check_if_variance_is_respected :
+  option variance -> rewrite_direction -> rewrite_direction ->  Prop :=
+  | MSNone : forall dir dir', check_if_variance_is_respected None dir dir'
+  | MSCovariant : forall dir, check_if_variance_is_respected (Some Covariant) dir dir
+  | MSContravariant :
+    forall 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).
+Defined.
+
+Definition relation_class_of_areflexive_relation_class:
+  Areflexive_Relation_Class -> Relation_Class.
+  induction 1.
+    exact (SymmetricAreflexive _ s).
+    exact (AsymmetricAreflexive tt Aeq).
+Defined.
+
+Definition carrier_of_reflexive_relation_class :=
+  fun 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).
+
+Definition relation_of_areflexive_relation_class :=
+  fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R).
+
+Inductive Morphism_Context Hole dir : Relation_Class -> rewrite_direction ->  Type :=
+  | App :
+    forall 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 :
+    forall S dir',
+      carrier_of_reflexive_relation_class S ->
+      Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir'
+  | ProperElementToKeep :
+    forall 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 :
+   rewrite_direction -> Arguments -> Type
+:=
+    fcl_singl :
+      forall 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)
+ | fcl_cons :
+      forall 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'' (necons S L).
+
+Scheme Morphism_Context_rect2 := Induction for Morphism_Context  Sort Type
+with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type.
+
+Definition product_of_arguments : Arguments -> Type.
+  induction 1.
+  exact (carrier_of_relation_class a).
+  exact (prod (carrier_of_relation_class a) IHX).
+Defined.
+
+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 *)
+Defined.
+
+Definition directed_relation_of_relation_class:
+  forall 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).
+Defined.
+
+Definition directed_relation_of_argument_class:
+  forall 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)).
+Defined.
+
+
+Definition relation_of_product_of_arguments:
+  forall dir 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).
+Defined. 
+
+Definition apply_morphism:
+  forall 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).
+Defined.
+
+Theorem apply_morphism_compatibility_Right2Left:
+  forall 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.
+
+Theorem apply_morphism_compatibility_Left2Right:
+  forall 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).
+Proof.
+  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.
+
+Definition interp :
+ forall 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 <-
+       (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
+       exact X.
+       exact X0.
+Defined.
+
+(* 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 :
+  forall 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 <-
+    (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
+    exact X.
+  exact X0.
+Defined.
+
+Theorem setoid_rewrite:
+  forall Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
+    (E: Morphism_Context Hole dir Out dir'),
+    (directed_relation_of_relation_class dir Hole E1 E2) ->
+    (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)).
+Proof.
+  intros.
+  elim E using
+    (@Morphism_Context_rect2 Hole dir
+      (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E))
+      (fun dir'' L fcl =>
+        relation_of_product_of_arguments dir'' _
+        (interp_relation_class_list E1 fcl)
+        (interp_relation_class_list E2 fcl))); intros.
+  change (directed_relation_of_relation_class dir'0 Out0
+    (apply_morphism _ _ (Function m) (interp_relation_class_list E1 m0))
+    (apply_morphism _ _ (Function m) (interp_relation_class_list E2 m0))).
+  destruct dir'0.
+    apply apply_morphism_compatibility_Left2Right.
+      exact (Compat m).
+      exact H0.
+    apply apply_morphism_compatibility_Right2Left.
+      exact (Compat m).
+      exact H0.
+
+  exact H.
+
+  unfold interp, Morphism_Context_rect2.
+  (* CSC: reflexivity used here *)
+  destruct S; destruct dir'0; simpl; (apply r || reflexivity).
+  
+  destruct dir'0; exact r.
+
+  destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
+    unfold get_rewrite_direction; simpl.
+  destruct dir'0; destruct dir'';
+    (exact H0 ||
+      unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
+  (* the following mess with generalize/clear/intros is to help Coq resolving *)
+  (* second order unification problems.                                       *)
+  generalize m c H0; clear H0 m c; inversion c;
+    generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
+      (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
+  destruct dir'0; destruct dir'';
+    (exact H0 ||
+      unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
+  (* the following mess with generalize/clear/intros is to help Coq resolving *)
+  (* second order unification problems.                                       *)
+  generalize m c H0; clear H0 m c; inversion c;
+    generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
+      (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3).
+  destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
+
+  change
+    (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
+       (eq_rect _ (fun T : Type => T) (interp E1 m) _
+         (about_carrier_of_relation_class_and_relation_class_of_argument_class S))
+       (eq_rect _ (fun T : Type => T) (interp E2 m) _
+         (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
+       relation_of_product_of_arguments dir'' _
+       (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
+  split.
+  clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl.
+    destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
+      inversion c.
+        rewrite <- H3; exact H0.
+        rewrite (opposite_direction_idempotent dir'0); exact H0.
+      destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
+      inversion c.
+        rewrite <- H3; exact H0.
+        rewrite (opposite_direction_idempotent dir'0); exact H0.
+      destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
+    exact H1.
+  Qed.