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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/T/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/T/props.ma
index 9e1bb8cfd..faa9ed95d 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/T/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/T/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/T/defs.ma".
+include "Basic-1/T/defs.ma".
 
 theorem not_abbr_abst:
  not (eq B Abbr Abst)
@@ -23,6 +23,9 @@ theorem not_abbr_abst:
 B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow True | 
 Abst \Rightarrow False | Void \Rightarrow False])) I Abst H) in (False_ind 
 False H0)).
+(* COMMENTS
+Initial nodes: 34
+END *)
 
 theorem not_void_abst:
  not (eq B Void Abst)
@@ -31,6 +34,9 @@ theorem not_void_abst:
 B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | 
 Abst \Rightarrow False | Void \Rightarrow True])) I Abst H) in (False_ind 
 False H0)).
+(* COMMENTS
+Initial nodes: 34
+END *)
 
 theorem not_abbr_void:
  not (eq B Abbr Void)
@@ -39,6 +45,9 @@ theorem not_abbr_void:
 B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow True | 
 Abst \Rightarrow False | Void \Rightarrow False])) I Void H) in (False_ind 
 False H0)).
+(* COMMENTS
+Initial nodes: 34
+END *)
 
 theorem not_abst_void:
  not (eq B Abst Void)
@@ -47,6 +56,9 @@ theorem not_abst_void:
 B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | 
 Abst \Rightarrow True | Void \Rightarrow False])) I Void H) in (False_ind 
 False H0)).
+(* COMMENTS
+Initial nodes: 34
+END *)
 
 theorem thead_x_y_y:
  \forall (k: K).(\forall (v: T).(\forall (t: T).((eq T (THead k v t) t) \to 
@@ -81,6 +93,9 @@ v (\lambda (t2: T).((eq T (THead k t2 t1) t1) \to (\forall (P0: Prop).P0)))
 H0 t0 H5) in (let H8 \def (eq_ind K k (\lambda (k1: K).((eq T (THead k1 t0 
 t1) t1) \to (\forall (P0: Prop).P0))) H7 k0 H6) in (H8 H4 P)))))) H3)) 
 H2))))))))) t))).
+(* COMMENTS
+Initial nodes: 461
+END *)
 
 theorem tweight_lt:
  \forall (t: T).(lt O (tweight t))
@@ -90,4 +105,7 @@ nat).(le_n (S O))) (\lambda (_: nat).(le_n (S O))) (\lambda (_: K).(\lambda
 (t0: T).(\lambda (H: (lt O (tweight t0))).(\lambda (t1: T).(\lambda (_: (lt O 
 (tweight t1))).(le_S (S O) (plus (tweight t0) (tweight t1)) (le_plus_trans (S 
 O) (tweight t0) (tweight t1) H))))))) t).
+(* COMMENTS
+Initial nodes: 85
+END *)