X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=weblib%2Fbasics%2Flogic.ma;h=3f92d6aad834d81fdc0bc2bd803f2cb41f85f998;hb=cf367920b94b3a95c5c068c2f0672b97bf579731;hp=374947b7d96bbfedaaea2925d26e8a26b37db54a;hpb=e0433942a61cfe8b43b68a81efa7d7d68abe3c5a;p=helm.git

diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index 374947b7d..3f92d6aad 100644
--- a/weblib/basics/logic.ma
+++ b/weblib/basics/logic.ma
@@ -56,7 +56,7 @@ theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. xA title="leibnitz's equality" href="
 (* deleterio per auto? *)
 theorem eq_f2: ∀A,B,C.∀f:A→B→C.
 ∀x1,x2:A.∀y1,y2:B. x1A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax2 → y1A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ay2 → f x1 y1 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A f x2 y2.
-#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 E1; E2; //; qed. 
+#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed. 
 
 (* hint to genereric equality 
 definition eq_equality: equality ≝