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

diff --git a/helm/software/matita/contribs/dama/dama/sandwich.ma b/helm/software/matita/contribs/dama/dama/sandwich.ma
index abccb351b..e55b6d3b3 100644
--- a/helm/software/matita/contribs/dama/dama/sandwich.ma
+++ b/helm/software/matita/contribs/dama/dama/sandwich.ma
@@ -38,10 +38,10 @@ unfold; simplify; exists [apply (a i)] split;
         [1: cases (us_phi4 ?? Gw 〈(a i),l〉); apply H2; clear H2 H;
             apply (Hma i); rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;
         |2: apply Hmb; apply (le_w_plus ma); assumption] 
-    |2: simplify; apply (le_transitive ???? Lax Lxb);
+    |2: simplify; apply (le_transitive (a i) ?? Lax Lxb);
     |3: simplify; repeat split; try assumption; 
-        [1: apply (le_transitive ???? Lax Lxb);
-        |2: intro X; cases (os_coreflexive ?? X)]]
+        [1: apply (le_transitive ?? (b i) Lax Lxb);
+        |2: intro X; cases (exc_coreflexive (a i) 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;]]