-H8) (le_n (plus O (S (minus n h))))) (le_O_n x1))) (ty3_abbr g (minus n h) e
-d0 u (getl_drop_conf_ge n (CHead d0 (Bind Abbr) u) c0 H1 e h x1 H5 H8) t H2))
-x0 H9))) H7)) H6)))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda
+H8) (le_plus_r O (S (minus n h)))) (le_O_n x1))) (ty3_abbr g (minus n h) e d0
+u (getl_drop_conf_ge n (CHead d0 (Bind Abbr) u) c0 H1 e h x1 H5 H8) t H2)) x0
+H9))) H7)) H6)))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda