added some missing includes

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / csubc / arity.ma

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 2cad21c833f4791a194deec0290902a3c3e747f7..53ab4989b340d010a87e29d2171e0d8ee1612714 100644 (file)
--- 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)))))))