]> matita.cs.unibo.it Git - helm.git/commit
advances on cofrees allows to prove one direction of
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 23 May 2014 17:30:04 +0000 (17:30 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 23 May 2014 17:30:04 +0000 (17:30 +0000)
commit8365510a374c2983c9546296b2337beaaa2866fa
tree75698f05e115d530fb5006dcc37afb78e6b5d31e
parent4b25f363cbe0bfc828f88972f1552c406ed31cbc
advances on cofrees allows to prove one direction of
non-recursive characterization of llpx_sn (finally!)
matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc [deleted file]
matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_nlift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lift_neg.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_alt.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
matita/matita/contribs/lambdadelta/ground_2/etc/lib/logic.etc [new file with mode: 0644]