X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2FC%2Fprops.ma;h=c93aa0f08ec8fbeba2699043682e1cc276b7517d;hb=89519c7b52e06304a94019dd528925300380cdc0;hp=30901423e2cb64a0a587cc36b586b778a5960af8;hpb=b58315ef220a130a44acbf528cd6885ddadad642;p=helm.git

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 30901423e..c93aa0f08 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma
@@ -14,26 +14,24 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/props".
+include "LambdaDelta-1/C/defs.ma".
 
-include "C/defs.ma".
-
-include "T/props.ma".
+include "LambdaDelta-1/T/props.ma".
 
 theorem clt_cong:
  \forall (c: C).(\forall (d: C).((clt c d) \to (\forall (k: K).(\forall (t: 
 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: