X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;h=6723cf2cc4bbca3d4a0797d50b8d97c8495d0fb2;hb=5a0bffcc89e1215ed051b515dc276f6b8111fc9d;hp=32124c2fbaaad21eb038bbb6d0e31e3feb70248e;hpb=92b9fb7c477eb1b0dbf5d921555d9a0295d0e46d;p=helm.git

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 32124c2fb..6723cf2cc 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -55,6 +55,10 @@ theorem eq_f2: ∀A,B,C.∀f:A→B→C.
 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
 #A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed. 
 
+lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
+∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = f x2 y2 z2.
+#A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
+
 (* hint to genereric equality 
 definition eq_equality: equality ≝
  mk_equality eq refl rewrite_l rewrite_r.