B).(\forall (e: C).(\forall (u: T).(P (CHead e (Bind b) u) (CHead e (Bind b)
u)))))) (f0: (\forall (e: C).(\forall (c: C).((clear e c) \to ((P e c) \to
(\forall (f0: F).(\forall (u: T).(P (CHead e (Flat f0) u) c)))))))) (c: C)
B).(\forall (e: C).(\forall (u: T).(P (CHead e (Bind b) u) (CHead e (Bind b)
u)))))) (f0: (\forall (e: C).(\forall (c: C).((clear e c) \to ((P e c) \to
(\forall (f0: F).(\forall (u: T).(P (CHead e (Flat f0) u) c)))))))) (c: C)