update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / tlist / props.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/tlist/props.ma b/matita/matita/contribs/lambdadelta/basic_1/tlist/props.ma
index f941820bbe7bfe6421042507c7469a5c934ca3e9..267f9d9ad45f18554c0b0180e416666294e00bed 100644 (file)
--- 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))))))