comment out an incomplete proof

diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index ed1caebe3b9607a96c29dca00fcb630b757eeb84..970a5e38892ae9a3b2c46c9ce92b81f7520fb2b2 100644 (file)
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -244,6 +244,7 @@ for @{ 'disjoint $a $b }.
 interpretation "Left cosets disjoint" 'disjoint C C' =
  (cic:/matita/algebra/groups/left_coset_disjoint.con _ C C').
 
+(*
 (* The following should be a one-shot alias! *)
 alias symbol "belongs_to" (instance 0) = "Belongs to subgroup".
 theorem foo:
@@ -267,6 +268,7 @@ exists;
 | 
 ].
 qed.
+*)
 
 (*theorem foo:
  \forall G:Group. \forall x1,x2:G. \forall H:subgroup G.
@@ -304,4 +306,4 @@ definition left_coset_eq ≝
     (element ? H)·(embed ? ? (subgroup_is_subgroup ? H) ˜ x) =
     (element ? H')·(embed ? ? (subgroup_is_subgroup ? H') ˜ y)).
 *)
-*)
\ No newline at end of file
+*)