From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 1 Apr 2005 11:06:01 +0000 (+0000)
Subject: initial version of the "lambda-delta" calculus including:
X-Git-Tag: after_svn_merge~40
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dabdf842f8f37da3d25a421740d141c28b23804a;p=helm.git

initial version of the "lambda-delta" calculus including:

- Confluence of reduction
- Generation lemma
- Thinning lemma
- Substitution lemma
- Type Correctness
- Type Uniqueness
- Subject Reduction
---

diff --git a/helm/coq-contribs/LAMBDA-TYPES.tgz b/helm/coq-contribs/LAMBDA-TYPES.tgz
new file mode 100644
index 000000000..93f106b51
Binary files /dev/null and b/helm/coq-contribs/LAMBDA-TYPES.tgz differ