]> matita.cs.unibo.it Git - helm.git/tree - matita/matita/contribs/lambdadelta/basic_2/syntax/
- tdeq must imply tsts
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / syntax /
drwxr-xr-x   ..
-rw-r--r-- 2916 aarity.ma
-rw-r--r-- 2739 append.ma
-rw-r--r-- 4692 append_length.ma
-rw-r--r-- 2223 cl_restricted_weight.ma
-rw-r--r-- 2180 cl_weight.ma
-rw-r--r-- 1943 genv.ma
-rw-r--r-- 3257 item.ma
-rw-r--r-- 4652 item_sd.ma
-rw-r--r-- 1899 item_sh.ma
-rw-r--r-- 3023 lenv.ma
-rw-r--r-- 2299 lenv_length.ma
-rw-r--r-- 1695 lenv_weight.ma
-rw-r--r-- 7152 tdeq.ma
-rw-r--r-- 2414 tdeq_tdeq.ma
-rw-r--r-- 5951 term.ma
-rw-r--r-- 1858 term_simple.ma
-rw-r--r-- 1762 term_vector.ma
-rw-r--r-- 1702 term_weight.ma
-rw-r--r-- 5861 tsts.ma
-rw-r--r-- 1579 tsts_simple.ma
-rw-r--r-- 1364 tsts_tdeq.ma
-rw-r--r-- 1786 tsts_tsts.ma
-rw-r--r-- 1622 tsts_vector.ma