update in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/flt/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/flt/fwd.ma
index c7720192a56ef6ddcb565318c8880dd3502b5270..a25e739167fd73ee260734166a89582dada254ad 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/flt/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/flt/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/flt/defs.ma".
 
-theorem flt_wf__q_ind:
+fact flt_wf__q_ind:
  \forall (P: ((C \to (T \to Prop)))).(((\forall (n: nat).((\lambda (P0: ((C 
 \to (T \to Prop)))).(\lambda (n0: nat).(\forall (c: C).(\forall (t: T).((eq 
 nat (fweight c t) n0) \to (P0 c t)))))) P n))) \to (\forall (c: C).(\forall 
@@ -28,7 +28,7 @@ nat (fweight c t) n0) \to (P0 c t)))))) P n))) \to (\forall (c: C).(\forall
 C).(\forall (t: T).((eq nat (fweight c t) n) \to (P c t))))))).(\lambda (c: 
 C).(\lambda (t: T).(H (fweight c t) c t (refl_equal nat (fweight c t))))))).
 
-theorem flt_wf_ind:
+lemma flt_wf_ind:
  \forall (P: ((C \to (T \to Prop)))).(((\forall (c2: C).(\forall (t2: 
 T).(((\forall (c1: C).(\forall (t1: T).((flt c1 t1 c2 t2) \to (P c1 t1))))) 
 \to (P c2 t2))))) \to (\forall (c: C).(\forall (t: T).(P c t))))