]> matita.cs.unibo.it Git - helm.git/tree - matita/matita/contribs/lambdadelta/basic_2/computation/
reaxiomatized lleq fixes a bug in it and allows to park substitution in etc
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation /
drwxr-xr-x   ..
-rw-r--r-- 2625 acp.ma
-rw-r--r-- 5141 acp_aaa.ma
-rw-r--r-- 8824 acp_cr.ma
-rw-r--r-- 2517 cpds.ma
-rw-r--r-- 1432 cpds_aaa.ma
-rw-r--r-- 3923 cpds_cpds.ma
-rw-r--r-- 1857 cpds_lift.ma
-rw-r--r-- 1930 cpre.ma
-rw-r--r-- 1583 cpre_cpre.ma
-rw-r--r-- 6593 cprs.ma
-rw-r--r-- 8741 cprs_cprs.ma
-rw-r--r-- 2804 cprs_lift.ma
-rw-r--r-- 1938 cpxe.ma
-rw-r--r-- 8124 cpxs.ma
-rw-r--r-- 1674 cpxs_aaa.ma
-rw-r--r-- 10577 cpxs_cpxs.ma
-rw-r--r-- 1368 cpxs_leq.ma
-rw-r--r-- 6163 cpxs_lift.ma
-rw-r--r-- 1962 cpxs_lleq.ma
-rw-r--r-- 5347 cpxs_tstc.ma
-rw-r--r-- 9026 cpxs_tstc_vector.ma
-rw-r--r-- 5926 csx.ma
-rw-r--r-- 3131 csx_aaa.ma
-rw-r--r-- 4958 csx_alt.ma
-rw-r--r-- 2037 csx_fpbs.ma
-rw-r--r-- 5432 csx_lift.ma
-rw-r--r-- 6710 csx_lpx.ma
-rw-r--r-- 1486 csx_lpxs.ma
-rw-r--r-- 5770 csx_tstc_vector.ma
-rw-r--r-- 2080 csx_vector.ma
-rw-r--r-- 1876 fpbc.ma
-rw-r--r-- 1544 fpbc_fpbs.ma
-rw-r--r-- 1988 fpbc_fpns.ma
-rw-r--r-- 3541 fpbg.ma
-rw-r--r-- 2803 fpbg_fpbg.ma
-rw-r--r-- 4115 fpbg_fpns.ma
-rw-r--r-- 1739 fpbg_lift.ma
-rw-r--r-- 7732 fpbs.ma
-rw-r--r-- 1618 fpbs_aaa.ma
-rw-r--r-- 3113 fpbs_alt.ma
-rw-r--r-- 1919 fpbs_ext.ma
-rw-r--r-- 1744 fpbs_fpbs.ma
-rw-r--r-- 1464 fpbs_fpns.ma
-rw-r--r-- 1707 fpbs_lift.ma
-rw-r--r-- 2548 fpbu.ma
-rw-r--r-- 3903 fpbu_fpns.ma
-rw-r--r-- 1872 fpbu_lift.ma
-rw-r--r-- 2049 fpns.ma
-rw-r--r-- 1481 fpns_fpns.ma
-rw-r--r-- 2283 fsb.ma
-rw-r--r-- 3886 fsb_aaa.ma
-rw-r--r-- 4010 fsb_alt.ma
-rw-r--r-- 3528 fsb_csx.ma
-rw-r--r-- 3635 lcosx.ma
-rw-r--r-- 3795 lcosx_cpxs.ma
-rw-r--r-- 3232 lprs.ma
-rw-r--r-- 2409 lprs_alt.ma
-rw-r--r-- 6845 lprs_cprs.ma
-rw-r--r-- 1569 lprs_ldrop.ma
-rw-r--r-- 1595 lprs_lprs.ma
-rw-r--r-- 3553 lpxs.ma
-rw-r--r-- 1743 lpxs_aaa.ma
-rw-r--r-- 2510 lpxs_alt.ma
-rw-r--r-- 7963 lpxs_cpxs.ma
-rw-r--r-- 1593 lpxs_ldrop.ma
-rw-r--r-- 6647 lpxs_lleq.ma
-rw-r--r-- 1279 lpxs_lpxs.ma
-rw-r--r-- 5028 lsubc.ma
-rw-r--r-- 3675 lsubc_ldrop.ma
-rw-r--r-- 1870 lsubc_ldrops.ma
-rw-r--r-- 1535 lsubc_lsuba.ma
-rw-r--r-- 4399 lsx.ma
-rw-r--r-- 3133 lsx_csx.ma
-rw-r--r-- 3983 lsx_ldrop.ma
-rw-r--r-- 5901 lsx_lpxs.ma