X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Fgroups.ma;h=d6e77ae8d0fa6a36404b7d084911e12602c234de;hb=8d961585c4ff785d558d5b4c84adf656595ca487;hp=29324c4aa748f9d4cf4f8b6d215c6d23f59bb2e0;hpb=80ea6f314e89d9d280338c41860cb04949319629;p=helm.git

diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index 29324c4aa..d6e77ae8d 100644
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -218,8 +218,8 @@ definition left_coset_eq ≝
  λG.λC,C':left_coset G.
   ∀x.((element ? C)·x \sub (subgrp ? C)) ∈ C'.
   
-interpretation "Left cosets equality" 'eq C C' =
- (cic:/matita/algebra/groups/left_coset_eq.con _ C C').
+interpretation "Left cosets equality" 'eq t C C' =
+ (cic:/matita/algebra/groups/left_coset_eq.con t C C').
 
 definition left_coset_disjoint ≝
  λG.λC,C':left_coset G.
@@ -287,7 +287,7 @@ theorem in_x_mk_left_coset_x_H:
  ∀G.∀x:Type_OF_Group G.∀H:subgroup G.x ∈ (x*H).
 intros;
 simplify;
-apply (ex_intro ? ? 1);
+apply (ex_intro ? ? ⅇ);
 rewrite > morphism_to_eq_f_1_1;
 rewrite > (e_is_right_unit ? G);
 reflexivity.