X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Farity%2Faprem.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Farity%2Faprem.ma;h=5045207ec1f78984da49648e2f5fedd70fc8f6f4;hb=20377cd037f6cc5eb9c6a5664354a8a0189d3f4f;hp=bfcc4fab3a940f977718724a02473b3ca4b49512;hpb=289d8d049e72beef41c17930f13727b5049981a2;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma
index bfcc4fab3..5045207ec 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma
@@ -20,8 +20,6 @@ include "LambdaDelta-1/arity/cimp.ma".
 
 include "LambdaDelta-1/aprem/props.ma".
 
-include "LambdaDelta-1/aprem/fwd.ma".
-
 theorem arity_aprem:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t 
 a) \to (\forall (i: nat).(\forall (b: A).((aprem i a b) \to (ex2_3 C T nat