From: matitaweb Date: Wed, 7 Sep 2011 14:04:31 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~2311 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=41d5d6bbe0214bac728a708d34ab3e0b4cac86db;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 ≝