update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / tlt / fwd.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/tlt/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/tlt/fwd.ma
index 2ee88a07352526ffaa66f2ac0b22738bd2af649d..f53eb19dcb143f8db2bac44fe0afc6fcb308822c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/tlt/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/tlt/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/tlt/defs.ma".
 
-theorem tlt_wf__q_ind:
+fact tlt_wf__q_ind:
  \forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P0: ((T \to 
 Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P0 
 t))))) P n))) \to (\forall (t: T).(P t)))
@@ -27,7 +27,7 @@ Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t)
 n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight 
 t)))))).
 
-theorem tlt_wf_ind:
+lemma tlt_wf_ind:
  \forall (P: ((T \to Prop))).(((\forall (t: T).(((\forall (v: T).((tlt v t) 
 \to (P v)))) \to (P t)))) \to (\forall (t: T).(P t)))
 \def