]> 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 70d16259901c6cc78ca43a2b9afa3cb986ab4bce..d64855d0d386850c6e86a9ddd560b3366803754d 100644 (file)
@@ -168,19 +168,11 @@ 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