]> matita.cs.unibo.it Git - helm.git/tree - matita/matita/contribs/lambdadelta/basic_2/substitution/
- advances on hereditarily free variables: now "frees" is primitive
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution /
drwxr-xr-x   ..
-rw-r--r-- 7444 cpys.ma
-rw-r--r-- 5325 cpys_alt.ma
-rw-r--r-- 6716 cpys_cpys.ma
-rw-r--r-- 11501 cpys_lift.ma
-rw-r--r-- 2036 fleq.ma
-rw-r--r-- 1901 fleq_fleq.ma
-rw-r--r-- 5570 fqup.ma
-rw-r--r-- 1287 fqup_fqup.ma
-rw-r--r-- 4335 fqus.ma
-rw-r--r-- 3209 fqus_alt.ma
-rw-r--r-- 1287 fqus_fqus.ma
-rw-r--r-- 7118 frees.ma
-rw-r--r-- 3597 frees_lift.ma
-rw-r--r-- 3228 gr2.ma
-rw-r--r-- 1575 gr2_gr2.ma
-rw-r--r-- 3616 gr2_minus.ma
-rw-r--r-- 1771 gr2_plus.ma
-rw-r--r-- 4558 ldrops.ma
-rw-r--r-- 2006 ldrops_ldrop.ma
-rw-r--r-- 1474 ldrops_ldrops.ma
-rw-r--r-- 6041 lifts.ma
-rw-r--r-- 3162 lifts_lift.ma
-rw-r--r-- 1889 lifts_lift_vector.ma
-rw-r--r-- 1468 lifts_lifts.ma
-rw-r--r-- 2621 lifts_vector.ma
-rw-r--r-- 7125 lleq.ma
-rw-r--r-- 2243 lleq_alt.ma
-rw-r--r-- 3128 lleq_alt_rec.ma
-rw-r--r-- 3705 lleq_fqus.ma
-rw-r--r-- 7808 lleq_ldrop.ma
-rw-r--r-- 1971 lleq_leq.ma
-rw-r--r-- 1739 lleq_lleq.ma
-rw-r--r-- 1908 lleq_llor.ma
-rw-r--r-- 1998 llor.ma
-rw-r--r-- 1323 llor_ldrop.ma
-rw-r--r-- 10459 llpx_sn.ma
-rw-r--r-- 3492 llpx_sn_alt.ma
-rw-r--r-- 13045 llpx_sn_alt_rec.ma
-rw-r--r-- 23235 llpx_sn_ldrop.ma
-rw-r--r-- 3068 llpx_sn_leq.ma
-rw-r--r-- 1918 llpx_sn_llor.ma
-rw-r--r-- 2017 llpx_sn_lpx_sn.ma
-rw-r--r-- 1537 llpx_sn_tc.ma