...

diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index 374947b7d96bbfedaaea2925d26e8a26b37db54a..3f92d6aad834d81fdc0bc2bd803f2cb41f85f998 100644 (file)
--- 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. x\ 5A title="leibnitz's equality" href="
 (* deleterio per auto? *)
 theorem eq_f2: ∀A,B,C.∀f:A→B→C.
 ∀x1,x2:A.∀y1,y2:B. x1\ 5A title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/A\ 6x2 → y1\ 5A title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/A\ 6y2 → f x1 y1 \ 5A title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/A\ 6 f x2 y2.
-#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 \ 6E1; \ 6E2; //; qed. 
+#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed. 
 
 (* hint to genereric equality 
 definition eq_equality: equality ≝