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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/tlist/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/tlist/props.ma
index 2a56bb13a..92b0d05ff 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/tlist/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/tlist/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/tlist/defs.ma".
+include "Basic-1/tlist/defs.ma".
 
 theorem tslt_wf__q_ind:
  \forall (P: ((TList \to Prop))).(((\forall (n: nat).((\lambda (P0: ((TList 
@@ -26,6 +26,9 @@ TList).((eq nat (tslen ts) n) \to (P ts))))) in (\lambda (P: ((TList \to
 Prop))).(\lambda (H: ((\forall (n: nat).(\forall (ts: TList).((eq nat (tslen 
 ts) n) \to (P ts)))))).(\lambda (ts: TList).(H (tslen ts) ts (refl_equal nat 
 (tslen ts)))))).
+(* COMMENTS
+Initial nodes: 61
+END *)
 
 theorem tslt_wf_ind:
  \forall (P: ((TList \to Prop))).(((\forall (ts2: TList).(((\forall (ts1: 
@@ -44,6 +47,9 @@ m))))).(\lambda (ts0: TList).(\lambda (H1: (eq nat (tslen ts0) n0)).(let H2
 (\forall (ts1: TList).((eq nat (tslen ts1) m) \to (P ts1)))))) H0 (tslen ts0) 
 H1) in (H ts0 (\lambda (ts1: TList).(\lambda (H3: (lt (tslen ts1) (tslen 
 ts0))).(H2 (tslen ts1) H3 ts1 (refl_equal nat (tslen ts1))))))))))))) ts)))).
+(* COMMENTS
+Initial nodes: 179
+END *)
 
 theorem theads_tapp:
  \forall (k: K).(\forall (v: T).(\forall (t: T).(\forall (vs: TList).(eq T 
@@ -56,6 +62,9 @@ k t0 (THead k v t)))) (refl_equal T (THead k v t)) (\lambda (t0: T).(\lambda
 v t)))).(eq_ind T (THeads k (TApp t1 v) t) (\lambda (t2: T).(eq T (THead k t0 
 (THeads k (TApp t1 v) t)) (THead k t0 t2))) (refl_equal T (THead k t0 (THeads 
 k (TApp t1 v) t))) (THeads k t1 (THead k v t)) H)))) vs)))).
+(* COMMENTS
+Initial nodes: 175
+END *)
 
 theorem tcons_tapp_ex:
  \forall (ts1: TList).(\forall (t1: T).(ex2_2 TList T (\lambda (ts2: 
@@ -90,6 +99,9 @@ TList).(\lambda (t2: T).(eq TList (TCons t1 (TApp x0 x1)) (TApp ts2 t2))))
 (\lambda (ts2: TList).(\lambda (_: T).(eq nat (S (tslen x0)) (tslen ts2)))) 
 (TCons t1 x0) x1 (refl_equal TList (TApp (TCons t1 x0) x1)) (refl_equal nat 
 (tslen (TCons t1 x0)))) (tslen t0) H2) (TCons t t0) H1))))) H0))))))) ts1).
+(* COMMENTS
+Initial nodes: 503
+END *)
 
 theorem tlist_ind_rev:
  \forall (P: ((TList \to Prop))).((P TNil) \to (((\forall (ts: 
@@ -113,4 +125,7 @@ T).(\lambda (H4: (eq TList (TCons t t0) (TApp x0 x1))).(\lambda (H5: (eq nat
 t1)) (H0 x0 x1 (H2 x0 (eq_ind nat (tslen t0) (\lambda (n: nat).(lt n (tslen 
 (TCons t t0)))) (le_n (tslen (TCons t t0))) (tslen x0) H5))) (TCons t t0) 
 H4))))) H3))))))) ts2)) ts)))).
+(* COMMENTS
+Initial nodes: 273
+END *)