uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / T / props.ma

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 9e1bb8cfd01ef6927811a49855c9046358c81286..faa9ed95d7ec8092b848ae861ff3da8b52e2b7e3 100644 (file)
--- 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 *)