X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsn3%2Ffwd.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsn3%2Ffwd.ma;h=68276fe9f7ef2c7212276ac9b990913798a8459b;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=26a719b58d3e14b79759a33a105d85e01ae99363;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/fwd.ma
index 26a719b58..68276fe9f 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/fwd.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/sn3/defs.ma".
+include "Basic-1/sn3/defs.ma".
 
-include "LambdaDelta-1/pr3/props.ma".
+include "Basic-1/pr3/props.ma".
 
 theorem sn3_gen_bind:
  \forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t: T).((sn3 c 
@@ -70,6 +70,9 @@ t2 H7) x t2 (refl_equal T (THead (Bind b) x t2))) in (land_ind (sn3 c x) (sn3
 (CHead c (Bind b) x) t2) (sn3 (CHead c (Bind b) x) t2) (\lambda (_: (sn3 c 
 x)).(\lambda (H10: (sn3 (CHead c (Bind b) x) t2)).H10)) H8))))))))))))))) y 
 H0))))) H))))).
+(* COMMENTS
+Initial nodes: 1055
+END *)
 
 theorem sn3_gen_flat:
  \forall (f: F).(\forall (c: C).(\forall (u: T).(\forall (t: T).((sn3 c 
@@ -119,6 +122,9 @@ T).((eq T x0 t0) \to (\forall (P0: Prop).P0))) H6 x0 H9) in (H11 (refl_equal
 T x0) P)))))) (pr3_thin_dx c x0 t2 H7 x f) x t2 (refl_equal T (THead (Flat f) 
 x t2))) in (land_ind (sn3 c x) (sn3 c t2) (sn3 c t2) (\lambda (_: (sn3 c 
 x)).(\lambda (H10: (sn3 c t2)).H10)) H8))))))))))))))) y H0))))) H))))).
+(* COMMENTS
+Initial nodes: 925
+END *)
 
 theorem sn3_gen_head:
  \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).((sn3 c 
@@ -134,6 +140,9 @@ F).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (sn3 c (THead
 (Flat f) u t))).(let H_x \def (sn3_gen_flat f c u t H) in (let H0 \def H_x in 
 (land_ind (sn3 c u) (sn3 c t) (sn3 c u) (\lambda (H1: (sn3 c u)).(\lambda (_: 
 (sn3 c t)).H1)) H0)))))))) k).
+(* COMMENTS
+Initial nodes: 191
+END *)
 
 theorem sn3_gen_cflat:
  \forall (f: F).(\forall (c: C).(\forall (u: T).(\forall (t: T).((sn3 (CHead 
@@ -148,6 +157,9 @@ t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 (CHead c (Flat f) u) t1 t2) \to
 (sn3 c t2)))))).(sn3_sing c t1 (\lambda (t2: T).(\lambda (H2: (((eq T t1 t2) 
 \to (\forall (P: Prop).P)))).(\lambda (H3: (pr3 c t1 t2)).(H1 t2 H2 
 (pr3_cflat c t1 t2 H3 f u))))))))) t H))))).
+(* COMMENTS
+Initial nodes: 175
+END *)
 
 theorem sn3_gen_lift:
  \forall (c1: C).(\forall (t: T).(\forall (h: nat).(\forall (d: nat).((sn3 c1 
@@ -179,4 +191,7 @@ d H9)) in (let H11 \def (eq_ind_r T t2 (\lambda (t0: T).((eq T x t0) \to
 (\forall (P0: Prop).P0))) H7 x (lift_inj x t2 h d H9)) in (H11 (refl_equal T 
 x) P))))) (pr3_lift c1 c2 h d H4 x t2 H8) t2 (refl_equal T (lift h d t2)) c2 
 H4)))))))))))))) y H0)))) H))))).
+(* COMMENTS
+Initial nodes: 565
+END *)