c u)).(\lambda (_: (sn3 (CHead c (Bind b) u) t)).H1)) H0)))))))) (\lambda (f:
F).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (sn3 c (THead
(Flat f) u t))).(let H_x \def (sn3_gen_flat f c u t H) in (let H0 \def H_x in
c u)).(\lambda (_: (sn3 (CHead c (Bind b) u) t)).H1)) H0)))))))) (\lambda (f:
F).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (sn3 c (THead
(Flat f) u t))).(let H_x \def (sn3_gen_flat f c u t H) in (let H0 \def H_x in