(d2: C).(\lambda (_: T).(csuba g d2 d1))) x2 x3 (drop_drop (Flat f) n x0
(CHead x2 (Bind Void) x3) H10 x1) H11)))))) H9)) H8)) c2 H6))))) H5)))))) k
H2 (drop_gen_drop k c (CHead d1 (Bind Abbr) u1) t n H1)))))))))))) c1)))) i).
(d2: C).(\lambda (_: T).(csuba g d2 d1))) x2 x3 (drop_drop (Flat f) n x0
(CHead x2 (Bind Void) x3) H10 x1) H11)))))) H9)) H8)) c2 H6))))) H5)))))) k
H2 (drop_gen_drop k c (CHead d1 (Bind Abbr) u1) t n H1)))))))))))) c1)))) i).