X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Ftlist%2Fprops.ma;h=267f9d9ad45f18554c0b0180e416666294e00bed;hb=8de8cf8adfa6fcda91047eb2c25535893ede046a;hp=f941820bbe7bfe6421042507c7469a5c934ca3e9;hpb=d2caaf419cb6c92cb5ca8615f8eac4e12f3ab728;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/tlist/props.ma b/matita/matita/contribs/lambdadelta/basic_1/tlist/props.ma
index f941820bb..267f9d9ad 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/tlist/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/tlist/props.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/tlist/defs.ma".
 
-theorem theads_tapp:
+lemma theads_tapp:
  \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
@@ -28,7 +28,7 @@ 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:
+lemma tcons_tapp_ex:
  \forall (ts1: TList).(\forall (t1: T).(ex2_2 TList T (\lambda (ts2: 
 TList).(\lambda (t2: T).(eq TList (TCons t1 ts1) (TApp ts2 t2)))) (\lambda 
 (ts2: TList).(\lambda (_: T).(eq nat (tslen ts1) (tslen ts2))))))