From afcc82e79c1ebddaaed0fe9e83cfcea79493701c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 26 Mar 2007 13:24:27 +0000
Subject: [PATCH] added eta expansion to avoid universe inconsistency.

---
 .../matita/library/technicalities/setoids.ma  | 34 +++++++++++++------
 1 file changed, 23 insertions(+), 11 deletions(-)

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index b2376f17d..4374ab113 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -68,17 +68,34 @@ definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
  [1,2,3,4,5: exact T1]
 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 1 (T1); apply (eq T1). 
+    (* this eta expansion is needed to avoid a universe inconsistency *)
  ]
 qed.
 
+definition relation_of_relation_classCOQ:
+ ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
+ intros 2;
+ exact (
+ match
+  R 
+  return
+    (λ x.carrier_of_relation_class X x -> carrier_of_relation_class X x -> Prop)
+with [
+ SymmetricReflexive A Aeq _ _ => Aeq
+| AsymmetricReflexive _ A Aeq _ => Aeq
+| SymmetricAreflexive A Aeq _ => Aeq
+| AsymmetricAreflexive _ A Aeq => Aeq
+| Leibniz T => 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) =
@@ -570,17 +587,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.
-- 
2.39.2