X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fpr0%2Fprops.ma;h=d7f69d691abb71849d095ce10739f316e6dd9c78;hb=86d3a559b94a16c571ca05defdcada6bae4cc14d;hp=7e0cd81903d5461ab62d4f2081a44eb4f645e15d;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/props.ma
index 7e0cd8190..d7f69d691 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pr0/defs.ma".
+include "Basic-1/pr0/defs.ma".
 
-include "LambdaDelta-1/subst0/subst0.ma".
+include "Basic-1/subst0/subst0.ma".
 
 theorem pr0_lift:
  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (h: nat).(\forall 
@@ -126,6 +126,9 @@ nat).(eq_ind_r T (THead (Flat Cast) (lift h d u) (lift h (s (Flat Cast) d)
 t3)) (\lambda (t: T).(pr0 t (lift h d t4))) (pr0_tau (lift h (s (Flat Cast) 
 d) t3) (lift h d t4) (H1 h d) (lift h d u)) (lift h d (THead (Flat Cast) u 
 t3)) (lift_head (Flat Cast) u t3 h d))))))))) t1 t2 H))).
+(* COMMENTS
+Initial nodes: 2845
+END *)
 
 theorem pr0_subst0_back:
  \forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst0 
@@ -177,6 +180,9 @@ t3) t)) (\lambda (t: T).(pr0 t (THead k u3 t4)))) (\lambda (x0: T).(\lambda
 (t: T).(subst0 i0 u0 (THead k u1 t3) t)) (\lambda (t: T).(pr0 t (THead k u3 
 t4))) (THead k x0 x) (subst0_both u0 u1 x0 i0 H7 k t3 x H5) (pr0_comp x0 u3 
 H8 x t4 H6 k))))) (H1 u0 H4))))) (H3 u0 H4))))))))))))))) i u2 t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 979
+END *)
 
 theorem pr0_subst0_fwd:
  \forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst0 
@@ -228,6 +234,9 @@ t3) t)) (\lambda (t: T).(pr0 (THead k u3 t4) t))) (\lambda (x0: T).(\lambda
 (t: T).(subst0 i0 u0 (THead k u1 t3) t)) (\lambda (t: T).(pr0 (THead k u3 t4) 
 t)) (THead k x0 x) (subst0_both u0 u1 x0 i0 H7 k t3 x H5) (pr0_comp u3 x0 H8 
 t4 x H6 k))))) (H1 u0 H4))))) (H3 u0 H4))))))))))))))) i u2 t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 979
+END *)
 
 theorem pr0_subst0:
  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (v1: T).(\forall 
@@ -1743,4 +1752,7 @@ T).(pr0 (THead (Flat Cast) x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))
 x (pr0_tau x1 x H9 x0) H10))))) H8)) (H1 v1 x1 (s (Flat Cast) i) H7 v2 H3)) 
 w1 H5)))))) H4)) (subst0_gen_head (Flat Cast) v1 u t3 w1 i H2))))))))))))) t1 
 t2 H))).
+(* COMMENTS
+Initial nodes: 38857
+END *)