(\forall (c: C).(P O O c c))) (f0: (\forall (k: K).(\forall (h: nat).(\forall
(c: C).(\forall (e: C).((drop (r k h) O c e) \to ((P (r k h) O c e) \to
(\forall (u: T).(P (S h) O (CHead c k u) e))))))))) (f1: (\forall (k:
(\forall (c: C).(P O O c c))) (f0: (\forall (k: K).(\forall (h: nat).(\forall
(c: C).(\forall (e: C).((drop (r k h) O c e) \to ((P (r k h) O c e) \to
(\forall (u: T).(P (S h) O (CHead c k u) e))))))))) (f1: (\forall (k: