From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 17 Jul 2008 13:27:14 +0000 (+0000)
Subject: 1 => \\e
X-Git-Tag: make_still_working~4917
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e9f9d6d7a0466ee132553fb7a983eac282fb12f;p=helm.git

1 => \\e
---

diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index 29324c4aa..f257951bc 100644
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -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.