some more work

[helm.git] / helm / software / matita / nlibrary / basics / functions.ma

diff --git a/helm/software/matita/nlibrary/basics/functions.ma b/helm/software/matita/nlibrary/basics/functions.ma
index a4a8f240d5e89d8c10866956f9c8010e5a6d8146..186aee41da4c943cc2d092ebdc4a58d530f9c2e6 100644 (file)
--- 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.