]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
- we introduced the pointer_step rc in the perspective of proving
[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / basic_1.txt
index 87bf34936f8142b0d0590e47c55591fd47ae6cee..d64855d0d386850c6e86a9ddd560b3366803754d 100644 (file)
@@ -78,22 +78,10 @@ csubc/arity csubc_arity_trans
 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
@@ -180,29 +168,14 @@ pc3/props pc3_eta
 
 pr0/fwd pr0_gen_void
 pr0/dec nf0_dec
-pr0/subst1 pr0_subst1_back
-pr0/subst1 pr0_subst1_fwd
-pr1/pr1 pr1_strip
-pr1/pr1 pr1_confluence
-pr1/props pr1_pr0
-pr1/props pr1_t
-pr1/props pr1_head_1
-pr1/props pr1_head_2
-pr1/props pr1_comp
+
 pr1/props pr1_eta
+
 pr2/fwd pr2_gen_void
 pr3/fwd pr3_gen_void
-pr3/pr1 pr3_pr1
 pr3/props pr3_eta
 sn3/props sns3_lifts
 sty1/cnt sty1_cnt
-sty1/props sty1_trans
-sty1/props sty1_bind
-sty1/props sty1_appl
-sty1/props sty1_lift
-sty1/props sty1_correct
-sty1/props sty1_abbr
-sty1/props sty1_cast2
 subst/fwd subst_sort
 subst/fwd subst_lref_lt
 subst/fwd subst_lref_eq
@@ -221,9 +194,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/fwd ty3_gen_appl
 ty3/fwd tys3_gen_nil
 ty3/fwd tys3_gen_cons
 ty3/fwd_nf2 ty3_gen_appl_nf2