Level-1/LambdaDelta now compiles fine

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / flt / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/props.ma
index 93edf90624e5214f315bf0adfc7a1c8d3eb33335..4602f2c6db3f365bbf9a7017e08814279c163a80 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/props.ma
@@ -97,9 +97,9 @@ t2)) (S O)) H (le_S_n (plus (cweight c2) (S O)) (plus (plus (cweight c2)
 t2)) (le_n (S O)))))))))))))).
 
 theorem flt_wf__q_ind:
- \forall (P: ((C \to (T \to Prop)))).(((\forall (n: nat).((\lambda (P: ((C 
+ \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 (P c t)))))) P n))) \to (\forall (c: C).(\forall 
+nat (fweight c t) n0) \to (P0 c t)))))) P n))) \to (\forall (c: C).(\forall 
 (t: T).(P c t))))
 \def
  let Q \def (\lambda (P: ((C \to (T \to Prop)))).(\lambda (n: nat).(\forall 
@@ -120,9 +120,9 @@ T).(((\forall (c1: C).(\forall (t1: T).((flt c1 t1 c2 t2) \to (P c1 t1)))))
 \to (P c2 t2)))))).(\lambda (c: C).(\lambda (t: T).(flt_wf__q_ind P (\lambda 
 (n: nat).(lt_wf_ind n (Q P) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: 
 nat).((lt m n0) \to (Q P m))))).(\lambda (c0: C).(\lambda (t0: T).(\lambda 
-(H1: (eq nat (fweight c0 t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n: 
-nat).(\forall (m: nat).((lt m n) \to (\forall (c: C).(\forall (t: T).((eq nat 
-(fweight c t) m) \to (P c t))))))) H0 (fweight c0 t0) H1) in (H c0 t0 
+(H1: (eq nat (fweight c0 t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n1: 
+nat).(\forall (m: nat).((lt m n1) \to (\forall (c1: C).(\forall (t1: T).((eq 
+nat (fweight c1 t1) m) \to (P c1 t1))))))) H0 (fweight c0 t0) H1) in (H c0 t0 
 (\lambda (c1: C).(\lambda (t1: T).(\lambda (H3: (flt c1 t1 c0 t0)).(H2 
 (fweight c1 t1) H3 c1 t1 (refl_equal nat (fweight c1 t1))))))))))))))) c 
 t))))).