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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/pr3_props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/pr3_props.ma
index 20d795000..b5bb1fb69 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/pr3_props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/pr3_props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/ty3/pr3.ma".
+include "Basic-1/ty3/pr3.ma".
 
 theorem ty3_cred_pr2:
  \forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (v2: T).((pr2 c v1 
@@ -40,6 +40,9 @@ c0) t1 t2 H1 (Bind b)) t0 (pr0_refl t0)) d u (S i) (getl_clear_bind b (CHead
 c0 (Bind b) t2) c0 t2 (clear_bind b c0 t2) (CHead d (Bind Abbr) u) i H0) 
 (CHead c0 (Bind b) t) (csubst0_snd_bind b i u t2 t H2 c0)))))))))))))))) c v1 
 v2 H))))).
+(* COMMENTS
+Initial nodes: 383
+END *)
 
 theorem ty3_cred_pr3:
  \forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (v2: T).((pr3 c v1 
@@ -57,6 +60,9 @@ B).(\forall (t4: T).(\forall (t5: T).((ty3 g (CHead c (Bind b) t2) t4 t5) \to
 (ty3 g (CHead c (Bind b) t3) t4 t5))))))).(\lambda (b: B).(\lambda (t0: 
 T).(\lambda (t4: T).(\lambda (H3: (ty3 g (CHead c (Bind b) t1) t0 t4)).(H2 b 
 t0 t4 (ty3_cred_pr2 g c t1 t2 H0 b t0 t4 H3)))))))))))) v1 v2 H))))).
+(* COMMENTS
+Initial nodes: 215
+END *)
 
 theorem ty3_gen_lift:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h: 
@@ -442,6 +448,9 @@ Cast) x5 x2)) (lift_flat Cast x5 x2 h x1)) (ty3_cast g e x3 x2 (ty3_conv g e
 x2 x5 H21 x3 x4 H18 (pc3_gen_lift c0 x4 x2 h x1 H17 e H6)) x5 H21))))) 
 H19))))) H16)))) t3 H8))))) x0 H7)))))) (lift_gen_flat Cast t3 t2 x0 h x1 
 H5))))))))))))))) c y x H0))))) H))))))).
+(* COMMENTS
+Initial nodes: 9781
+END *)
 
 theorem ty3_tred:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u 
@@ -452,6 +461,9 @@ t1) \to (\forall (t2: T).((pr3 c t1 t2) \to (ty3 g c u t2)))))))
 (\lambda (t: T).(ty3 g c t1 t)) (ty3 g c u t2) (\lambda (x: T).(\lambda (H1: 
 (ty3 g c t1 x)).(let H_y \def (ty3_sred_pr3 c t1 t2 H0 g x H1) in (ty3_conv g 
 c t2 x H_y u t1 H (pc3_pr3_r c t1 t2 H0))))) (ty3_correct g c u t1 H)))))))).
+(* COMMENTS
+Initial nodes: 121
+END *)
 
 theorem ty3_sconv_pc3:
  \forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c 
@@ -465,6 +477,9 @@ u2 t2)).(\lambda (H1: (pc3 c u1 u2)).(let H2 \def H1 in (ex2_ind T (\lambda
 T).(\lambda (H3: (pr3 c u1 x)).(\lambda (H4: (pr3 c u2 x)).(let H_y \def 
 (ty3_sred_pr3 c u2 x H4 g t2 H0) in (let H_y0 \def (ty3_sred_pr3 c u1 x H3 g 
 t1 H) in (ty3_unique g c x t1 H_y0 t2 H_y)))))) H2)))))))))).
+(* COMMENTS
+Initial nodes: 141
+END *)
 
 theorem ty3_sred_back:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t0: T).((ty3 g c 
@@ -477,6 +492,9 @@ t) \to (ty3 g c t1 t)))))))))
 t3)) (ty3 g c t1 t) (\lambda (x: T).(\lambda (H2: (ty3 g c t x)).(ty3_conv g 
 c t x H2 t1 t0 H (ty3_unique g c t2 t0 (ty3_sred_pr3 c t1 t2 H0 g t0 H) t 
 H1)))) (ty3_correct g c t2 t H1)))))))))).
+(* COMMENTS
+Initial nodes: 137
+END *)
 
 theorem ty3_sconv:
  \forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c 
@@ -489,4 +507,7 @@ u2 t2)).(\lambda (H1: (pc3 c u1 u2)).(let H2 \def H1 in (ex2_ind T (\lambda
 (t: T).(pr3 c u1 t)) (\lambda (t: T).(pr3 c u2 t)) (ty3 g c u1 t2) (\lambda 
 (x: T).(\lambda (H3: (pr3 c u1 x)).(\lambda (H4: (pr3 c u2 x)).(ty3_sred_back 
 g c u1 t1 H x H3 t2 (ty3_sred_pr3 c u2 x H4 g t2 H0))))) H2)))))))))).
+(* COMMENTS
+Initial nodes: 129
+END *)