From 2833624d7e2bfea7525f75acd1e9284080eb6ea8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Dec 2006 16:37:06 +0000 Subject: [PATCH] added some missing includes --- .../LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma | 2 ++ .../LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma | 2 ++ .../contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma | 4 ++++ .../contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma | 6 ++++++ 4 files changed, 14 insertions(+) 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))))))) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma index 783c668e6..c2e0ad1d8 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma @@ -22,6 +22,8 @@ include "sc3/props.ma". include "csuba/defs.ma". +include "csuba/props.ma". + theorem csubc_csuba: \forall (g: G).(\forall (c1: C).(\forall (c2: C).((csubc g c1 c2) \to (csuba g c1 c2)))) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma index e8c5f04ae..dc6d76656 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma @@ -17,6 +17,10 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity". include "csubc/props.ma". +include "csubc/getl.ma". +include "csubc/arity.ma". +include "lift1/props.ma". +include "csubc/drop1.ma". theorem sc3_arity_csubc: \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1 diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma index aa28b068b..bde89cd02 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma @@ -30,6 +30,12 @@ include "llt/props.ma". include "drop1/props.ma". +include "lift1/props.ma". + +include "drop1/getl.ma". + +include "csuba/arity.ma". + theorem sc3_arity_gen: \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((sc3 g a c t) \to (arity g c t a))))) -- 2.39.2