X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Ftlist%2Fprops.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Ftlist%2Fprops.ma;h=fd6e7db98c23dea4554f5cac130d0c1dfcfae135;hb=6329f0f87906d3347c39d2ba2f5ec2b2124f17a2;hp=6ee6bf5d803c7cd7e6504cbf1c8881f0f46d4683;hpb=783fbc6eb42d5db260d93d8d213a7d5c035e99e3;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma
index 6ee6bf5d8..fd6e7db98 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-
+set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/props".
 
 include "tlist/defs.ma".
 
@@ -48,18 +48,16 @@ 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)))).
 
 theorem theads_tapp:
- \forall (k: K).(\forall (vs: TList).(\forall (v: T).(\forall (t: T).(eq T 
+ \forall (k: K).(\forall (v: T).(\forall (t: T).(\forall (vs: TList).(eq T 
 (THeads k (TApp vs v) t) (THeads k vs (THead k v t))))))
 \def
- \lambda (k: K).(\lambda (vs: TList).(TList_ind (\lambda (t: TList).(\forall 
-(v: T).(\forall (t0: T).(eq T (THeads k (TApp t v) t0) (THeads k t (THead k v 
-t0)))))) (\lambda (v: T).(\lambda (t: T).(refl_equal T (THead k v t)))) 
-(\lambda (t: T).(\lambda (t0: TList).(\lambda (H: ((\forall (v: T).(\forall 
-(t1: T).(eq T (THeads k (TApp t0 v) t1) (THeads k t0 (THead k v 
-t1))))))).(\lambda (v: T).(\lambda (t1: T).(eq_ind_r T (THeads k t0 (THead k 
-v t1)) (\lambda (t2: T).(eq T (THead k t t2) (THead k t (THeads k t0 (THead k 
-v t1))))) (refl_equal T (THead k t (THeads k t0 (THead k v t1)))) (THeads k 
-(TApp t0 v) t1) (H v t1))))))) vs)).
+ \lambda (k: K).(\lambda (v: T).(\lambda (t: T).(\lambda (vs: 
+TList).(TList_ind (\lambda (t0: TList).(eq T (THeads k (TApp t0 v) t) (THeads 
+k t0 (THead k v t)))) (refl_equal T (THead k v t)) (\lambda (t0: T).(\lambda 
+(t1: TList).(\lambda (H: (eq T (THeads k (TApp t1 v) t) (THeads k t1 (THead k 
+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)))).
 
 theorem tcons_tapp_ex:
  \forall (ts1: TList).(\forall (t1: T).(ex2_2 TList T (\lambda (ts2: 
@@ -95,7 +93,7 @@ TList).(\lambda (t2: T).(eq TList (TCons t1 (TApp x0 x1)) (TApp ts2 t2))))
 (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).
 
-theorem tlist_ind_rew:
+theorem tlist_ind_rev:
  \forall (P: ((TList \to Prop))).((P TNil) \to (((\forall (ts: 
 TList).(\forall (t: T).((P ts) \to (P (TApp ts t)))))) \to (\forall (ts: 
 TList).(P ts))))