X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fpc3%2Fdec.ma;h=c8cca31319c94a239d2cac541c2928799504cd25;hp=aa7a4d89e29bee58e72cf0ad1c2ddbf32a99cd4e;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hpb=88a68a9c334646bc17314d5327cd3b790202acd6

diff --git a/matita/matita/contribs/lambdadelta/basic_1/pc3/dec.ma b/matita/matita/contribs/lambdadelta/basic_1/pc3/dec.ma
index aa7a4d89e..c8cca3131 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/pc3/dec.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pc3/dec.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/ty3/arity_props.ma".
+include "basic_1/ty3/arity_props.ma".
 
-include "Basic-1/nf2/fwd.ma".
+include "basic_1/nf2/fwd.ma".
 
 theorem pc3_dec:
  \forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c 
@@ -49,9 +49,6 @@ x2)).(let H_y1 \def (nf2_pr3_unfold c x0 x2 H14 H6) in (let H16 \def
 (eq_ind_r T x2 (\lambda (t: T).(pr3 c x1 t)) H15 x0 H_y1) in (let H17 \def 
 (nf2_pr3_confluence c x H3 x0 H6 u1 H2) in (H8 (H17 (pr3_t x1 u1 c H11 x0 
 H16)) False))))))) H13)))))) H10))))) H7)))))) H4)))))) H1)))))))))))).
-(* COMMENTS
-Initial nodes: 551
-END *)
 
 theorem pc3_abst_dec:
  \forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c 
@@ -146,7 +143,4 @@ Abst) x5) x6)).(let H32 \def (nf2_pr3_confluence c x0 H8 x5 H30 u2 H7) in
 (Bind Abst)) (H32 (pr3_t x3 u2 c H20 x5 H25)) (refl_equal T x6))) False)))) 
 H29))))))))) H23)))))))) H18))))))) (pr3_confluence c u1 x1 H13 x H4))))) 
 H12)))))) H9)))))) H6)))))) H3)))))))))))).
-(* COMMENTS
-Initial nodes: 1759
-END *)