u)))) (\lambda (c1: C).(drop h d c1 c2)) x0 (clear_flat x (CHead x0 (Bind b)
(lift h d u)) H7 f (lift h (r (Flat f) d) t)) H8)))) H6))))) k H1 H3) x1
H2)))) (drop_gen_skip_r c x1 t h d k H0)))))))))))))) x2).
u)))) (\lambda (c1: C).(drop h d c1 c2)) x0 (clear_flat x (CHead x0 (Bind b)
(lift h d u)) H7 f (lift h (r (Flat f) d) t)) H8)))) H6))))) k H1 H3) x1
H2)))) (drop_gen_skip_r c x1 t h d k H0)))))))))))))) x2).