[(Bind _) \Rightarrow f | (Flat f1) \Rightarrow f1])) (Flat f) (Flat f0) H1)
in (let H3 \def (eq_ind_r F f0 (\lambda (f1: F).((eq F f f1) \to (\forall
(P0: Prop).P0))) H0 f H2) in (H3 (refl_equal F f) P))))))) H)))) k2))) k1).
[(Bind _) \Rightarrow f | (Flat f1) \Rightarrow f1])) (Flat f) (Flat f0) H1)
in (let H3 \def (eq_ind_r F f0 (\lambda (f1: F).((eq F f f1) \to (\forall
(P0: Prop).P0))) H0 f H2) in (H3 (refl_equal F f) P))))))) H)))) k2))) k1).