\forall (i: nat).(\forall (a: C).(\forall (c: C).((getl i c a) \to (\forall
(e: C).(\forall (h: nat).((getl h c e) \to ((le h i) \to (getl (minus i h) e
a))))))))
\forall (i: nat).(\forall (a: C).(\forall (c: C).((getl i c a) \to (\forall
(e: C).(\forall (h: nat).((getl h c e) \to ((le h i) \to (getl (minus i h) e
a))))))))