proposition: Lemma mem_drop_inv : forall l i x, mem x (drop i l) -> 0 <= i <= length l -> mem x l.
proof: Proof. Proof using. introv Hx Hi. rewrites* <- (>> list_eq_take_app_drop i). apply* mem_app_r. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)