From 0e9f9d6d7a0466ee132553fb7a983eac282fb12f Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 17 Jul 2008 13:27:14 +0000
Subject: [PATCH 1/1] 1 => \\e

---
 helm/software/matita/library/algebra/groups.ma | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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.
-- 
2.39.2