X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fbasics%2Ffunctions.ma;h=186aee41da4c943cc2d092ebdc4a58d530f9c2e6;hb=27c34e93fc35402111253325b93089a6308dd4bb;hp=a4a8f240d5e89d8c10866956f9c8010e5a6d8146;hpb=3bd88fb8b932e2f76762e8068b19745167cb1ce1;p=helm.git

diff --git a/helm/software/matita/nlibrary/basics/functions.ma b/helm/software/matita/nlibrary/basics/functions.ma
index a4a8f240d..186aee41d 100644
--- a/helm/software/matita/nlibrary/basics/functions.ma
+++ b/helm/software/matita/nlibrary/basics/functions.ma
@@ -36,11 +36,12 @@ ndefinition symmetric2: ∀A,B:Type[0].∀f:A→A→B.Prop
 ndefinition associative: ∀A:Type[0].∀f:A→A→A.Prop
 ≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
 
+(*
 ntheorem eq_f_g_h:
   ∀A,B,C,D:Type[0].∀f:C→D.∀g:B→C.∀h:A→B.
   f∘(g∘h) = (f∘g)∘h.
   //.
-nqed.
+nqed. *)
 
 (* functions and relations *)
 ndefinition monotonic : ∀A:Type.∀R:A→A→Prop.