(getl n c1 e)))) (\lambda (e: C).(\lambda (H1: (getl n c1 e)).H1)) (\lambda
(c3: C).(\lambda (H1: (csubst0 i v c1 c3)).(\lambda (e: C).(\lambda (H2:
(getl n c3 e)).(csubst0_getl_ge_back i n H c1 c3 v H1 e H2))))) c2 H0))))))).
(getl n c1 e)))) (\lambda (e: C).(\lambda (H1: (getl n c1 e)).H1)) (\lambda
(c3: C).(\lambda (H1: (csubst0 i v c1 c3)).(\lambda (e: C).(\lambda (H2:
(getl n c3 e)).(csubst0_getl_ge_back i n H c1 c3 v H1 e H2))))) c2 H0))))))).