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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/fwd.ma
index fe6666a1d..1a18f7dbc 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/fwd.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pr2/defs.ma".
+include "Basic-1/pr2/defs.ma".
 
-include "LambdaDelta-1/pr0/fwd.ma".
+include "Basic-1/pr0/fwd.ma".
 
-include "LambdaDelta-1/getl/drop.ma".
+include "Basic-1/getl/drop.ma".
 
-include "LambdaDelta-1/getl/clear.ma".
+include "Basic-1/getl/clear.ma".
 
 theorem pr2_gen_sort:
  \forall (c: C).(\forall (x: T).(\forall (n: nat).((pr2 c (TSort n) x) \to 
@@ -43,6 +43,9 @@ t2)) H2 (TSort n) H4) in (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T t t0))
 (let H6 \def (eq_ind T t2 (\lambda (t0: T).(subst0 i u t0 t)) H3 (TSort n) 
 (pr0_gen_sort t2 n H5)) in (subst0_gen_sort u t i n H6 (eq T t (TSort n)))) 
 t1 H4))))))))))))) c y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 347
+END *)
 
 theorem pr2_gen_lref:
  \forall (c: C).(\forall (x: T).(\forall (n: nat).((pr2 c (TLRef n) x) \to 
@@ -93,6 +96,9 @@ u))) H1 n H7) in (or_intror (eq T (lift (S n) O u) (TLRef n)) (ex2_2 C T
 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T (lift (S n) O u) (lift (S 
 n) O u0)))) d u H9 (refl_equal T (lift (S n) O u))))) t H8))) 
 (subst0_gen_lref u t i n H6))) t1 H4))))))))))))) c y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 1003
+END *)
 
 theorem pr2_gen_abst:
  \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c 
@@ -215,6 +221,9 @@ H12) (\lambda (b: B).(\lambda (u0: T).(pr2_delta (CHead c0 (Bind b) u0) d u
 (S i) (getl_head (Bind b) i c0 (CHead d (Bind Abbr) u) H1 u0) t1 x1 H8 x3 
 H13)))) t H11)))))) H10)) (subst0_gen_head (Bind Abst) u x0 x1 t i H9)))))))) 
 (pr0_gen_abst u1 t1 t2 H5)))))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 2383
+END *)
 
 theorem pr2_gen_cast:
  \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c 
@@ -347,6 +356,9 @@ t1 t2)).(or_intror (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t
 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c0 t1 t3)))) (pr2 c0 t1 t) 
 (pr2_delta c0 d u i H1 t1 t2 H6 t H3))) (pr0_gen_cast u1 t1 t2 
 H5)))))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 2659
+END *)
 
 theorem pr2_gen_csort:
  \forall (t1: T).(\forall (t2: T).(\forall (n: nat).((pr2 (CSort n) t1 t2) 
@@ -364,6 +376,9 @@ t3 t4)).(\lambda (t: T).(\lambda (_: (subst0 i u t4 t)).(\lambda (H4: (eq C c
 (CSort n))).(let H5 \def (eq_ind C c (\lambda (c0: C).(getl i c0 (CHead d 
 (Bind Abbr) u))) H1 (CSort n) H4) in (getl_gen_sort n i (CHead d (Bind Abbr) 
 u) H5 (pr0 t3 t)))))))))))))) y t1 t2 H0))) H)))).
+(* COMMENTS
+Initial nodes: 221
+END *)
 
 theorem pr2_gen_appl:
  \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c 
@@ -2520,6 +2535,9 @@ i)))) x7 H19)))))) H18)) (subst0_gen_head (Flat Appl) u (lift (S O) O x3) x5
 x7 (s (Bind x0) i) H17)) t H15)))))) H14)) (subst0_gen_head (Bind x0) u x4 
 (THead (Flat Appl) (lift (S O) O x3) x5) t i H13)) t1 H8)))))))))))))) H6)) 
 (pr0_gen_appl u1 t1 t2 H5)))))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 38859
+END *)
 
 theorem pr2_gen_abbr:
  \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c 
@@ -3070,6 +3088,9 @@ B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))))
 (getl_head (Bind b) i c0 (CHead d (Bind Abbr) u) H1 u0) t1 (lift (S O) O t2) 
 H6 (lift (S O) O t) (subst0_lift_ge_S t2 t u i H3 O (le_O_n i))))))) 
 (pr0_gen_abbr u1 t1 t2 H5)))))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 11671
+END *)
 
 theorem pr2_gen_void:
  \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c 
@@ -3242,6 +3263,9 @@ B).(\lambda (u0: T).(pr2_delta (CHead c0 (Bind b) u0) d u (S i) (getl_head
 (Bind b) i c0 (CHead d (Bind Abbr) u) H1 u0) t1 (lift (S O) O t2) H6 (lift (S 
 O) O t) (subst0_lift_ge_S t2 t u i H3 O (le_O_n i))))))) (pr0_gen_void u1 t1 
 t2 H5)))))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 3467
+END *)
 
 theorem pr2_gen_lift:
  \forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h: nat).(\forall 
@@ -3313,4 +3337,7 @@ t3))) (\lambda (t3: T).(pr2 e t1 t3)) x1 H12 (pr2_delta e d0 u (minus i h)
 (getl_drop_conf_ge i (CHead d0 (Bind Abbr) u) c0 H1 e h d H5 H11) t1 x0 H8 x1 
 H13))))) (subst0_gen_lift_ge u x0 t i h d H9 H11)))))))))) (pr0_gen_lift t1 
 t2 h d H6)))))))))))))))) c y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1579
+END *)