From a03b64206ee8c1769adf987d08090d9b59ceefe1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 11 Jul 2006 08:06:53 +0000 Subject: [PATCH] fixed --- 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 884e0c582..9ab695239 100644 --- a/helm/software/matita/library/algebra/groups.ma +++ b/helm/software/matita/library/algebra/groups.ma @@ -296,7 +296,7 @@ qed. (*CSC: here the coercion Type_of_Group cannot be omitted. Why? *) theorem in_x_mk_left_coset_x_H: - ∀G.∀x:Type_of_Group G.∀H:subgroup G.x ∈ (x*H). + ∀G.∀x:Type_OF_Group G.∀H:subgroup G.x ∈ (x*H). intros; simplify; apply (ex_intro ? ? 1); -- 2.39.2