changelog to -rc-1

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

diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma
index b01bf12e1859d517cd220a0c6143eb5f222f35d3..a1880711dbe23e3d03bb444422ea7f3ad704ccb3 100644 (file)
--- 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).