X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fpc3%2Fdec.ma;h=aa7a4d89e29bee58e72cf0ad1c2ddbf32a99cd4e;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=74d45cd176532519bb6cc29494b44baa50a95b44;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/dec.ma
index 74d45cd17..aa7a4d89e 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/dec.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/dec.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/ty3/arity_props.ma".
+include "Basic-1/ty3/arity_props.ma".
 
-include "LambdaDelta-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,6 +49,9 @@ 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 
@@ -143,4 +146,7 @@ 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 *)