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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/props.ma
index bf9f641b0..579a8dd69 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/ty3/fwd.ma".
+include "Basic-1/ty3/fwd.ma".
 
-include "LambdaDelta-1/pc3/fwd.ma".
+include "Basic-1/pc3/fwd.ma".
 
 theorem ty3_lift:
  \forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((ty3 g e 
@@ -180,6 +180,9 @@ g c0 t (lift h d (THead (Flat Cast) t4 t3)))) (eq_ind_r T (THead (Flat Cast)
 Cast) d) h H4) (lift h d t4) (H3 c0 d h H4)) (lift h d (THead (Flat Cast) t4 
 t3)) (lift_head (Flat Cast) t4 t3 h d)) (lift h d (THead (Flat Cast) t3 t0)) 
 (lift_head (Flat Cast) t3 t0 h d)))))))))))))) e t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 4253
+END *)
 
 theorem ty3_correct:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c 
@@ -243,6 +246,9 @@ c0 t3 t)))).(\lambda (t4: T).(\lambda (H2: (ty3 g c0 t3 t4)).(\lambda (H3:
 Cast) t4 t3) t))) (\lambda (x: T).(\lambda (H5: (ty3 g c0 t4 x)).(ex_intro T 
 (\lambda (t: T).(ty3 g c0 (THead (Flat Cast) t4 t3) t)) (THead (Flat Cast) x 
 t4) (ty3_cast g c0 t3 t4 H2 x H5)))) H4)))))))))) c t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 1333
+END *)
 
 theorem ty3_unique:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u 
@@ -415,6 +421,9 @@ t4)).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (H7: (ty3 g c0 t2 x0)).(pc3_t
 (THead (Flat Cast) x0 t2) c0 (THead (Flat Cast) t3 t2) (pc3_head_1 c0 t3 x0 
 (H3 x0 H7) (Flat Cast) t2) t4 H5))))) (ty3_gen_cast g c0 t0 t2 t4 
 H4)))))))))))) c u t1 H))))).
+(* COMMENTS
+Initial nodes: 3459
+END *)
 
 theorem ty3_gen_abst_abst:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall 
@@ -446,6 +455,9 @@ c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2)) x3 H5
 (ty3_gen_bind g Abst c u t1 (THead (Bind Abst) u t2) H))))))) (ty3_gen_bind g 
 Abst c u t2 x H0)))) (ty3_correct g c (THead (Bind Abst) u t1) (THead (Bind 
 Abst) u t2) H))))))).
+(* COMMENTS
+Initial nodes: 571
+END *)
 
 theorem ty3_typecheck:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (v: T).((ty3 g c t 
@@ -457,6 +469,9 @@ T).(ty3 g c (THead (Flat Cast) v t) u))) (\lambda (x: T).(\lambda (H0: (ty3 g
 c v x)).(ex_intro T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u)) 
 (THead (Flat Cast) x v) (ty3_cast g c t v H x H0)))) (ty3_correct g c t v 
 H)))))).
+(* COMMENTS
+Initial nodes: 131
+END *)
 
 theorem ty3_getl_subst0:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t 
@@ -670,4 +685,7 @@ t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead
 x0)).(\lambda (_: (subst0 (s (Flat Cast) i) v0 t1 x1)).(H3 v0 x0 i H8 b d v 
 H5)))))) H6)) (subst0_gen_head (Flat Cast) v0 t2 t1 t3 i H4)))))))))))))))))) 
 c t u H))))).
+(* COMMENTS
+Initial nodes: 4343
+END *)