removed <_,_> notation second interpretation for dependent pair, since it used

[helm.git] / helm / software / matita / contribs / dama / dama / sandwich.ma

diff --git a/helm/software/matita/contribs/dama/dama/sandwich.ma b/helm/software/matita/contribs/dama/dama/sandwich.ma
index df66b8b8cb15e787d5cd814aa238fed0170e37c0..abccb351b14736ae1a0d7d276a228eb57937caf4 100644 (file)
--- 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;]]