.ma inclusions corrected/minimized

[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 71b6d84599df20cfcd223a7565e4c83bb85f03e5..da90d421177817ff8561794d66250f97c6ce4fda 100644 (file)
--- a/helm/matita/library/higher_order_defs/functions.ma
+++ b/helm/matita/library/higher_order_defs/functions.ma
@@ -15,7 +15,6 @@
 set "baseuri" "cic:/matita/higher_order_defs/functions/".
 
 include "logic/equality.ma".
-include "logic/connectives.ma".
 
 definition injective: \forall A,B:Type.\forall f:A \to B.Prop
 \def \lambda A,B.\lambda f.