proposition: Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l.
proof: Proof. destruct l as [|x1 [|x2 l]]; try reflexivity. unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l. generalize (λ x, hash x `mod` (2 * Z.of_nat (length l)))%Z; intros f. rewrite elem_of_elements; split. - revert x. induction l as [|y l IH]; intros x; simpl. { by rewrite elem_of_empty. } rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto. - induction 1; set_solver. Qed.
imports: stdpp(zmap) stdpp(options)