(H0: (drop (S O) i c1 c2)).(let H3 \def (eq_ind nat (minus (S i) (S O))
(\lambda (n: nat).(drop n O c2 e)) (drop_conf_ge (S i) e c1 (getl_drop b c1 e
u i H) c2 (S O) i H0 (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(le n (S
-i))) (le_n (S i)) (plus i (S O)) (plus_comm i (S O)))) i (minus_Sx_SO i)) in
+i))) (le_n (S i)) (plus i (S O)) (plus_sym i (S O)))) i (minus_Sx_SO i)) in
H3)))))))).
theorem getl_drop_conf_rev: