X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2FC%2Fprops.ma;h=30901423e2cb64a0a587cc36b586b778a5960af8;hb=b58315ef220a130a44acbf528cd6885ddadad642;hp=97926688359442e300d10e00cf2a3d6b0c0b77b0;hpb=354c363760b5d5222b82674fca38e9c0dc55010e;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 979266883..30901423e 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
@@ -25,18 +25,16 @@ 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).(lt_le_S (plus (cweight c) (tweight t)) 
-(plus (cweight d) (tweight t)) (plus_lt_compat_r (cweight c) (cweight d) 
-(tweight t) H)))))).
+d))).(\lambda (_: K).(\lambda (t: T).(plus_lt_compat_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)))) (lt_le_S (plus 
-(cweight c) O) (plus (cweight c) (tweight u)) (plus_le_lt_compat (cweight c) 
-(cweight c) O (tweight u) (le_n (cweight c)) (tweight_lt u))) (cweight c) 
-(plus_n_O (cweight c))))).
+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)) 
+(tweight_lt u)) (cweight c) (plus_n_O (cweight c))))).
 
 theorem clt_wf__q_ind:
  \forall (P: ((C \to Prop))).(((\forall (n: nat).((\lambda (P0: ((C \to