X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Ftheory.ma;h=423565e498d6271d03449a17c770e857b4fb932e;hb=ac51c1272a969de33bb3fcf75aa4c6e3f56d1721;hp=7f15aaf0882d01aa6c15858442c5d43da481555e;hpb=f97af72aec6f23053fff6f1a1f6b0a923dc584c9;p=helm.git diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma index 7f15aaf08..423565e49 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma @@ -80,6 +80,8 @@ include "drop1/defs.ma". include "drop1/props.ma". +include "drop1/getl.ma". + include "clear/defs.ma". include "clear/fwd.ma". @@ -98,15 +100,111 @@ include "getl/clear.ma". include "getl/drop.ma". +include "getl/getl.ma". + include "getl/dec.ma". include "getl/flt.ma". include "cimp/defs.ma". +include "cimp/props.ma". + +include "subst0/defs.ma". + +include "subst0/fwd.ma". + +include "subst0/props.ma". + +include "subst0/subst0.ma". + +include "subst0/tlt.ma". + +include "subst0/dec.ma". + +include "subst1/defs.ma". + +include "subst1/fwd.ma". + +include "subst1/props.ma". + +include "subst1/subst1.ma". + +include "csubst0/defs.ma". + +include "csubst0/fwd.ma". + +include "csubst0/props.ma". + +include "csubst0/drop.ma". + +include "csubst0/clear.ma". + +include "csubst0/getl.ma". + +include "csubst1/defs.ma". + +include "csubst1/fwd.ma". + +include "csubst1/props.ma". + +include "csubst1/getl.ma". + +include "fsubst0/defs.ma". + +include "fsubst0/fwd.ma". + include "G/defs.ma". include "next_plus/defs.ma". include "next_plus/props.ma". +include "tau0/defs.ma". + +include "tau0/props.ma". + +include "A/defs.ma". + +include "asucc/defs.ma". + +include "asucc/fwd.ma". + +include "aplus/defs.ma". + +include "aplus/props.ma". + +include "leq/defs.ma". + +include "leq/fwd.ma". + +include "leq/props.ma". + +include "leq/asucc.ma". + +include "llt/defs.ma". + +include "llt/props.ma". + +include "aprem/defs.ma". + +include "aprem/props.ma". + +include "gz/defs.ma". + +include "gz/props.ma". + +include "arity/defs.ma". + +include "arity/fwd.ma". + +include "arity/props.ma". + +include "arity/subst0.ma". + +include "arity/lift1.ma". + +include "arity/cimp.ma". + +include "arity/aprem.ma". +