proposition: Lemma drop_nil : forall n, drop n (@nil A) = nil.
proof: Proof. Proof using. intros. unfold drop. apply LibList.drop_nil. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)