]> matita.cs.unibo.it Git - helm.git/commitdiff
1 => \\e
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 17 Jul 2008 13:27:14 +0000 (13:27 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 17 Jul 2008 13:27:14 +0000 (13:27 +0000)
helm/software/matita/library/algebra/groups.ma

index 29324c4aa748f9d4cf4f8b6d215c6d23f59bb2e0..f257951bc4a031abb0a1640ac0c673da3e6b340c 100644 (file)
@@ -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.