x))).(\lambda (_: (lt x n0)).(drop_drop (Flat f) n0 c e (H12 x1 v H8 e H14)
t)))) H15)) (lt_gen_xS x2 n0 H13)))))) k H10 H11 (drop_gen_drop k x1 e x0 n0
H9)))))))))))) H4)) (csubst0_gen_head k c c2 t v i H2))))))))))) c1)))))) n).
x))).(\lambda (_: (lt x n0)).(drop_drop (Flat f) n0 c e (H12 x1 v H8 e H14)
t)))) H15)) (lt_gen_xS x2 n0 H13)))))) k H10 H11 (drop_gen_drop k x1 e x0 n0
H9)))))))))))) H4)) (csubst0_gen_head k c c2 t v i H2))))))))))) c1)))))) n).