support for candidates of reducibility started ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / Basic_1.txt

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
index f8c868a7159010208053712a389843528915d74d..b7fa79e70e83e88ee4aef5460fecfb3bf78285e5 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
@@ -265,15 +265,9 @@ pr1/props pr1_head_2
 pr1/props pr1_comp
 pr1/props pr1_eta
 pr2/clen pr2_gen_ctail
-pr2/subst1 pr2_gen_cabbr
-
-# check ######################################################################
-
 pr2/fwd pr2_gen_void
 pr2/props pr2_ctail
-
-# waiting ####################################################################
-
+pr2/subst1 pr2_gen_cabbr
 pr3/fwd pr3_gen_sort
 pr3/fwd pr3_gen_abst
 pr3/fwd pr3_gen_cast
@@ -374,9 +368,6 @@ sty1/props sty1_lift
 sty1/props sty1_correct
 sty1/props sty1_abbr
 sty1/props sty1_cast2
-subst0/dec dnf_dec2
-subst0/dec dnf_dec
-subst1/props subst1_ex
 subst/fwd subst_sort
 subst/fwd subst_lref_lt
 subst/fwd subst_lref_eq
@@ -384,11 +375,6 @@ subst/fwd subst_lref_gt
 subst/fwd subst_head
 subst/props subst_lift_SO
 subst/props subst_subst0
-T/dec terms_props__bind_dec
-T/dec bind_dec_not
-T/dec terms_props__flat_dec
-T/dec terms_props__kind_dec
-T/dec term_dec
 T/dec binder_dec
 T/dec abst_dec
 tlist/props tslt_wf__q_ind
@@ -396,12 +382,6 @@ tlist/props tslt_wf_ind
 tlist/props theads_tapp
 tlist/props tcons_tapp_ex
 tlist/props tlist_ind_rev
-T/props not_abbr_abst
-T/props not_void_abst
-T/props not_abbr_void
-T/props not_abst_void
-T/props thead_x_y_y
-T/props tweight_lt
 ty3/arity ty3_arity
 ty3/arity_props ty3_predicative
 ty3/arity_props ty3_repellent
@@ -466,3 +446,5 @@ wf3/ty3 wf3_pr2_conf
 wf3/ty3 wf3_pr3_conf
 wf3/ty3 wf3_pc3_conf
 wf3/ty3 wf3_ty3_conf
+
+# check ######################################################################