-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).