X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fclear%2Fprops.ma;h=a1880711dbe23e3d03bb444422ea7f3ad704ccb3;hb=1776f357e1a69fa1133956660b65d7bafdfe5c25;hp=b01bf12e1859d517cd220a0c6143eb5f222f35d3;hpb=14d370851b7779e9fc6343532372e939dadb831c;p=helm.git

diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma
index b01bf12e1..a1880711d 100644
--- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma
@@ -134,7 +134,6 @@ C).(\lambda (H0: (clear (CHead c k t) c2)).(K_ind (\lambda (k0: K).((clear
 (CHead c (Bind b) t) (\lambda (c0: C).(le (cweight c0) (plus (cweight c) 
 (tweight t)))) (le_n (plus (cweight c) (tweight t))) c2 (clear_gen_bind b c 
 c2 t H1)))) (\lambda (f: F).(\lambda (H1: (clear (CHead c (Flat f) t) 
-c2)).(le_S_n (cweight c2) (plus (cweight c) (tweight t)) (le_n_S (cweight c2) 
-(plus (cweight c) (tweight t)) (le_plus_trans (cweight c2) (cweight c) 
-(tweight t) (H c2 (clear_gen_flat f c c2 t H1))))))) k H0))))))) c1).
+c2)).(le_plus_trans (cweight c2) (cweight c) (tweight t) (H c2 
+(clear_gen_flat f c c2 t H1))))) k H0))))))) c1).