]> matita.cs.unibo.it Git - helm.git/commit
- some new auxiliary lemmas
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 13 Oct 2007 15:22:37 +0000 (15:22 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 13 Oct 2007 15:22:37 +0000 (15:22 +0000)
commitb58315ef220a130a44acbf528cd6885ddadad642
tree753396fa85c3d6486521d920e2d7f812e07a38f4
parent354c363760b5d5222b82674fca38e9c0dc55010e
- some new auxiliary lemmas
- some improved proofs
37 files changed:
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/gz/defs.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/gz/props.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma