X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fsandwich.ma;h=abccb351b14736ae1a0d7d276a228eb57937caf4;hb=59f65aaf6f8d23748e1294ecabffffaa903ae657;hp=df66b8b8cb15e787d5cd814aa238fed0170e37c0;hpb=cb4d4678ada706caaf8c54f2d6780c228645f911;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/sandwich.ma b/helm/software/matita/contribs/dama/dama/sandwich.ma
index df66b8b8c..abccb351b 100644
--- a/helm/software/matita/contribs/dama/dama/sandwich.ma
+++ b/helm/software/matita/contribs/dama/dama/sandwich.ma
@@ -41,7 +41,7 @@ unfold; simplify; exists [apply (a i)] split;
     |2: simplify; apply (le_transitive ???? Lax Lxb);
     |3: simplify; repeat split; try assumption; 
         [1: apply (le_transitive ???? Lax Lxb);
-        |2: (* prove le_reflexive *) intro X; cases (os_coreflexive ?? X)]]
+        |2: intro X; cases (os_coreflexive ?? X)]]
 |1: apply HW; exists[apply l] simplify; split;
     [1: apply (us_phi1 ?? Gw); unfold; apply eq_reflexive;
     |2: apply Hma;  rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;]]