]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma
components/library: dotdothack removed
[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / arity / aprem.ma
index bfcc4fab3a940f977718724a02473b3ca4b49512..5045207ec1f78984da49648e2f5fedd70fc8f6f4 100644 (file)
@@ -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