From 54e4a83ab2bcfd6d051036d8c37f475494575fab Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 22 Dec 2006 14:54:38 +0000 Subject: [PATCH] - sc3/props.ma sc3/arity.ma: dependences fixed - csubc/arity.ma csubc/csuba.ma: reverted as no fix was needed --- .../LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma | 2 -- .../LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma | 2 -- .../LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma | 8 +++++--- .../LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma | 8 ++++---- 4 files changed, 9 insertions(+), 11 deletions(-) diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma index 53ab4989b..2cad21c83 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma @@ -20,8 +20,6 @@ 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/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma index c2e0ad1d8..783c668e6 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma @@ -22,8 +22,6 @@ 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/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma index dc6d76656..a347cc075 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma @@ -16,12 +16,14 @@ 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/getl.ma". + include "csubc/drop1.ma". +include "csubc/props.ma". + theorem sc3_arity_csubc: \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1 t a) \to (\forall (d1: C).(\forall (is: PList).((drop1 is d1 c1) \to (\forall diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma index bde89cd02..465a97ee7 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma @@ -22,20 +22,20 @@ include "sn3/lift1.ma". include "nf2/lift1.ma". +include "csuba/arity.ma". + include "arity/lift1.ma". include "arity/aprem.ma". include "llt/props.ma". +include "drop1/getl.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