*** empty log message ***

[helm.git] / helm / matita / library / higher_order_defs / functions.ma

diff --git a/helm/matita/library/higher_order_defs/functions.ma b/helm/matita/library/higher_order_defs/functions.ma
index d2a577a4912145a0621ced90440568fb039c4359..321ae46b7502c1578975b24ccdc25c4351065788 100644 (file)
--- a/helm/matita/library/higher_order_defs/functions.ma
+++ b/helm/matita/library/higher_order_defs/functions.ma
@@ -20,7 +20,6 @@ definition injective: \forall A,B:Type.\forall f:A \to B.Prop
 \def \lambda A,B.\lambda f.
   \forall x,y:A.f x = f y \to x=y.
 
-(* we have still to attach exists *)
 definition surjective: \forall A,B:Type.\forall f:A \to B.Prop
 \def \lambda A,B.\lambda f.
   \forall z:B. \exists x:A.z=f x.