From 41d5d6bbe0214bac728a708d34ab3e0b4cac86db Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 7 Sep 2011 14:04:31 +0000 Subject: [PATCH] ... --- weblib/basics/logic.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 ≝ -- 2.39.2