the generation of the multiple conjunction is now supported!

[helm.git] / matita / matita / lib / lambda-delta / syntax / weight.ma

diff --git a/matita/matita/lib/lambda-delta/syntax/weight.ma b/matita/matita/lib/lambda-delta/syntax/weight.ma
index 8d5ed68352678151054cbcdcfa262254d2a53ac9..d076dea9d68734c30b00667001d6a4eafd0b5032 100644 (file)
--- a/matita/matita/lib/lambda-delta/syntax/weight.ma
+++ b/matita/matita/lib/lambda-delta/syntax/weight.ma
@@ -35,6 +35,10 @@ definition cw: lenv → term → ? ≝ λL,T. #L + #T.
 
 interpretation "weight (closure)" 'Weight L T = (cw L T).
 
+axiom tw_wf_ind: ∀P:term→Prop.
+                 (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) →
+                 ∀T. P T.
+
 axiom cw_wf_ind: ∀P:lenv→term→Prop.
                  (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) →
                  ∀L,T. P L T.