X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fllt%2Ffwd.ma;h=8d45d3775af57733596afec64a06f79a4525a4f4;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=7cad4fc7a63ca276ddbf8afec411276e85017ff7;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/llt/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/llt/fwd.ma
index 7cad4fc7a..8d45d3775 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/llt/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/llt/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/llt/defs.ma".
 
-theorem llt_wf__q_ind:
+fact llt_wf__q_ind:
  \forall (P: ((A \to Prop))).(((\forall (n: nat).((\lambda (P0: ((A \to 
 Prop))).(\lambda (n0: nat).(\forall (a: A).((eq nat (lweight a) n0) \to (P0 
 a))))) P n))) \to (\forall (a: A).(P a)))
@@ -27,7 +27,7 @@ Prop))).(\lambda (H: ((\forall (n: nat).(\forall (a: A).((eq nat (lweight a)
 n) \to (P a)))))).(\lambda (a: A).(H (lweight a) a (refl_equal nat (lweight 
 a)))))).
 
-theorem llt_wf_ind:
+lemma llt_wf_ind:
  \forall (P: ((A \to Prop))).(((\forall (a2: A).(((\forall (a1: A).((llt a1 
 a2) \to (P a1)))) \to (P a2)))) \to (\forall (a: A).(P a)))
 \def