]> 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)
commitad1ff720d3d5f12daa001231682172779c1728f6
tree2fdbe789c9b1e55bfd6d32df24a919a4f792a50f
parentc44705de023d8a288a6792ac031e66ea007f2f96
- some new auxiliary lemmas
- some improved proofs
37 files changed:
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/gz/defs.ma [deleted file]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/gz/props.ma [deleted file]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma