X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fbasic_1.txt;h=c5fe6def0932a2c8fcf2db186caa9c28cdca7b8f;hb=69644bb333b2862a5ff2ff434df8830e854e3385;hp=92bd9860d94ebb3d96d834bbf32984128f15eea6;hpb=de64015de66a48373ade6cab7508d8f8e2c43af9;p=helm.git

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 92bd9860d..c5fe6def0 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -47,6 +47,7 @@ asucc/fwd asucc_gen_head
 cnt/props cnt_lift
 C/props clt_wf__q_ind
 C/props clt_wf_ind
+
 csuba/arity csuba_arity
 csuba/arity csuba_arity_rev
 csuba/arity arity_appls_appl
@@ -71,27 +72,16 @@ csuba/getl csuba_getl_abst
 csuba/getl csuba_getl_abst_rev
 csuba/getl csuba_getl_abbr_rev
 csuba/props csuba_refl
+
 csubc/arity csubc_arity_conf
 csubc/arity csubc_arity_trans
-csubc/csuba csubc_csuba
 csubc/drop1 drop1_csubc_trans
 csubc/drop drop_csubc_trans
-csubt/clear csubt_clear_conf
+
 csubt/csuba csubt_csuba
-csubt/drop csubt_drop_flat
-csubt/drop csubt_drop_abbr
-csubt/drop csubt_drop_abst
 csubt/fwd csubt_gen_abbr
 csubt/fwd csubt_gen_abst
-csubt/fwd csubt_gen_flat
-csubt/fwd csubt_gen_bind
-csubt/getl csubt_getl_abbr
-csubt/getl csubt_getl_abst
-csubt/pc3 csubt_pr2
-csubt/pc3 csubt_pc3
-csubt/props csubt_refl
-csubt/ty3 csubt_ty3
-csubt/ty3 csubt_ty3_ld
+
 csubv/clear csubv_clear_conf
 csubv/clear csubv_clear_conf_void
 csubv/drop csubv_drop_conf
@@ -110,7 +100,6 @@ ex1/props ex1_arity
 ex1/props ex1_ty3
 ex2/props ex2_nf2
 ex2/props ex2_arity
-fsubst0/fwd fsubst0_gen_base
 leq/asucc asucc_repl
 leq/asucc asucc_inj
 leq/asucc leq_asucc
@@ -167,23 +156,15 @@ pc1/props pc1_head
 
 pc3/dec pc3_dec
 pc3/dec pc3_abst_dec
-pc3/fsubst0 pc3_pr2_fsubst0
-pc3/fsubst0 pc3_pr2_fsubst0_back
-pc3/fsubst0 pc3_fsubst0
 pc3/fwd pc3_gen_not_abst
 pc3/fwd pc3_gen_lift_abst
 pc3/nf2 pc3_nf2
 pc3/nf2 pc3_nf2_unfold
 pc3/pc1 pc3_pc1
-pc3/props pc3_pr0_pr2_t
 pc3/props pc3_pr2_pr2_t
 pc3/props pc3_pr2_pr3_t
 pc3/props pc3_pr3_pc3_t
 pc3/props pc3_eta
-pc3/subst1 pc3_gen_cabbr
-pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
-pc3/wcpr0 pc3_wcpr0_t
-pc3/wcpr0 pc3_wcpr0
 
 pr0/fwd pr0_gen_void
 pr0/dec nf0_dec
@@ -198,19 +179,10 @@ pr1/props pr1_head_2
 pr1/props pr1_comp
 pr1/props pr1_eta
 pr2/fwd pr2_gen_void
-pr2/subst1 pr2_gen_cabbr
 pr3/fwd pr3_gen_void
 pr3/pr1 pr3_pr1
 pr3/props pr3_eta
-pr3/subst1 pr3_gen_cabbr
 sn3/props sns3_lifts
-sty0/fwd sty0_gen_sort
-sty0/fwd sty0_gen_lref
-sty0/fwd sty0_gen_bind
-sty0/fwd sty0_gen_appl
-sty0/fwd sty0_gen_cast
-sty0/props sty0_lift
-sty0/props sty0_correct
 sty1/cnt sty1_cnt
 sty1/props sty1_trans
 sty1/props sty1_bind
@@ -237,12 +209,7 @@ ty3/arity ty3_arity
 ty3/arity_props ty3_predicative
 ty3/arity_props ty3_repellent
 ty3/arity_props ty3_acyclic
-ty3/arity_props ty3_sn3
 ty3/dec ty3_inference
-ty3/fsubst0 ty3_fsubst0
-ty3/fsubst0 ty3_csubst0
-ty3/fsubst0 ty3_subst0
-ty3/fwd ty3_gen_appl
 ty3/fwd tys3_gen_nil
 ty3/fwd tys3_gen_cons
 ty3/fwd_nf2 ty3_gen_appl_nf2
@@ -267,11 +234,10 @@ ty3/pr3_props ty3_tred
 ty3/pr3_props ty3_sconv_pc3
 ty3/pr3_props ty3_sred_back
 ty3/pr3_props ty3_sconv
-ty3/props ty3_unique
 ty3/props ty3_gen_abst_abst
 ty3/sty0 ty3_sty0
-ty3/subst1 ty3_gen_cabbr
 ty3/subst1 ty3_gen_cvoid
+
 wf3/clear wf3_clear_conf
 wf3/clear clear_wf3_trans
 wf3/fwd wf3_gen_sort1