]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
closure property S4 added to abstract candidates of reducibility ...
[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / Basic_1.txt
index b7fa79e70e83e88ee4aef5460fecfb3bf78285e5..0d06d98b520959e088690f4274736136dde14128 100644 (file)
@@ -74,6 +74,9 @@ csuba/getl csuba_getl_abst
 csuba/getl csuba_getl_abst_rev
 csuba/getl csuba_getl_abbr_rev
 csuba/props csuba_refl
+
+# check #############################################################
+
 csubc/arity csubc_arity_conf
 csubc/arity csubc_arity_trans
 csubc/clear csubc_clear_conf
@@ -89,6 +92,9 @@ csubc/fwd csubc_gen_sort_r
 csubc/fwd csubc_gen_head_r
 csubc/getl csubc_getl_conf
 csubc/props csubc_refl
+
+# waiting ####################################################################
+
 csubt/clear csubt_clear_conf
 csubt/csuba csubt_csuba
 csubt/drop csubt_drop_flat
@@ -114,10 +120,8 @@ csubv/props csubv_bind_same
 csubv/props csubv_refl
 drop1/fwd drop1_gen_pnil
 drop1/fwd drop1_gen_pcons
-drop1/getl drop1_getl_trans
 drop1/props drop1_skip_bind
 drop1/props drop1_cons_tail
-drop1/props drop1_trans
 drop/props drop_ctail
 ex0/props aplus_gz_le
 ex0/props aplus_gz_ge
@@ -146,17 +150,10 @@ leq/props leq_sym
 leq/props leq_trans
 leq/props leq_ahead_false_1
 leq/props leq_ahead_false_2
-lift1/fwd lift1_sort
-lift1/fwd lift1_lref
-lift1/fwd lift1_bind
-lift1/fwd lift1_flat
 lift1/fwd lift1_cons_tail
 lift1/fwd lifts1_flat
 lift1/fwd lifts1_nil
 lift1/fwd lifts1_cons
-lift1/props lift1_lift1
-lift1/props lift1_xhg
-lift1/props lifts1_xhg
 lift1/props lift1_free
 lift/props thead_x_lift_y_y
 lift/props lifts_tapp