A failing unification of a coercion vs a term is now tried again after

[helm.git] / helm / matita / library / algebra / groups.ma

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index c93c9d94c9757e0d1f3cfdaaa2aac452e8c0272a..bec57fb4c2ca845a9d49bcd511c74b15a44e81bb 100644 (file)
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -104,13 +104,15 @@ record finite_enumerable (T:Type) : Type ≝
    repr_index_of: ∀x. repr (index_of x) = x
  }.
  
-notation < "hvbox(C \sub i)" with precedence 89
+notation "hvbox(C \sub i)" with precedence 89
 for @{ 'repr $C $i }.
 
+(* CSC: multiple interpretations in the same file are not considered in the
+ right order
 interpretation "Finite_enumerable representation" 'repr C i =
- (cic:/matita/algebra/groups/repr.con C _ i).
+ (cic:/matita/algebra/groups/repr.con C _ i).*)
  
-notation < "hvbox(|C|)" with precedence 89
+notation "hvbox(|C|)" with precedence 89
 for @{ 'card $C }.
 
 interpretation "Finite_enumerable order" 'card C =
@@ -159,11 +161,7 @@ theorem foo:
   right_cancellable ? (op G) →
    ∃e:G. isMonoid G e.
 intros;
-letin f ≝
- (λn.index_of G (is_finite_enumerable G)
-  (op G
-   (repr (Type_of_finite_enumerable_SemiGroup G) (is_finite_enumerable G) O)
-   (repr (Type_of_finite_enumerable_SemiGroup G) (is_finite_enumerable G) n)));
+letin f ≝ (λn.ι(G \sub O · G \sub n));
 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
 [ letin EX ≝ (Hcut O ?);
   [ apply le_O_n
@@ -175,7 +173,7 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
     clearbody HH;
     rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
-    apply (ex_intro ? ? (repr ? (is_finite_enumerable G) a));
+    apply (ex_intro ? ? (G \sub a));
     letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O));
     clearbody GOGO;
     rewrite < HH in GOGO;
@@ -186,13 +184,13 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     clear GOGO;
     constructor 1;
     [ unfold is_left_unit; intro;
-      letin GaxGax ≝ (refl_eq ? ((repr ? (is_finite_enumerable G) a)·x));
+      letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
       clearbody GaxGax;
       rewrite < GaGa in GaxGax:(? ? % ?);
       rewrite > (semigroup_properties G) in GaxGax;
       apply (H ? ? ? GaxGax)
     | unfold is_right_unit; intro;
-      letin GaxGax ≝ (refl_eq ? (x·(repr ? (is_finite_enumerable G) a)));
+      letin GaxGax ≝ (refl_eq ? (x·G \sub a));
       clearbody GaxGax;
       rewrite < GaGa in GaxGax:(? ? % ?);
       rewrite < (semigroup_properties G) in GaxGax;