\forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h
(S d) c e) \to (\forall (f: F).(\forall (u: T).(drop h (S d) (CHead c (Flat
f) (lift h (S d) u)) (CHead e (Flat f) u))))))))
\forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h
(S d) c e) \to (\forall (f: F).(\forall (u: T).(drop h (S d) (CHead c (Flat
f) (lift h (S d) u)) (CHead e (Flat f) u))))))))