Procedural : tentative update to the new letin cic construction

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma
index 907c5c373a8c2c30f3e135077374311d9402da97..c93aa0f08ec8fbeba2699043682e1cc276b7517d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma
@@ -23,15 +23,15 @@ theorem clt_cong:
 T).(clt (CHead c k t) (CHead d k t))))))
 \def
  \lambda (c: C).(\lambda (d: C).(\lambda (H: (lt (cweight c) (cweight 
-d))).(\lambda (_: K).(\lambda (t: T).(plus_lt_compat_r (cweight c) (cweight 
-d) (tweight t) H))))).
+d))).(\lambda (_: K).(\lambda (t: T).(lt_reg_r (cweight c) (cweight d) 
+(tweight t) H))))).
 
 theorem clt_head:
  \forall (k: K).(\forall (c: C).(\forall (u: T).(clt c (CHead c k u))))
 \def
  \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(eq_ind_r nat (plus (cweight 
 c) O) (\lambda (n: nat).(lt n (plus (cweight c) (tweight u)))) 
-(plus_le_lt_compat (cweight c) (cweight c) O (tweight u) (le_n (cweight c)) 
+(le_lt_plus_plus (cweight c) (cweight c) O (tweight u) (le_n (cweight c)) 
 (tweight_lt u)) (cweight c) (plus_n_O (cweight c))))).
 
 theorem clt_wf__q_ind: