X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Fcsubc%2Farity.ma;h=53ab4989b340d010a87e29d2171e0d8ee1612714;hb=2833624d7e2bfea7525f75acd1e9284080eb6ea8;hp=2cad21c833f4791a194deec0290902a3c3e747f7;hpb=9408f2869ddbbbae68dcb23ebf6c358c61888d0d;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma
index 2cad21c83..53ab4989b 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma
@@ -20,6 +20,8 @@ include "csubc/csuba.ma".
 
 include "arity/defs.ma".
 
+include "csuba/arity.ma".
+
 theorem csubc_arity_conf:
  \forall (g: G).(\forall (c1: C).(\forall (c2: C).((csubc g c1 c2) \to 
 (\forall (t: T).(\forall (a: A).((arity g c1 t a) \to (arity g c2 t a)))))))