Remove 'NoDup' lemma.

parent 512d7073
Pipeline #19063 failed with stage
in 0 seconds
......@@ -1112,14 +1112,6 @@ Section map_filter.
Lemma map_filter_empty : filter P ( : M A) = .
Proof. apply map_fold_empty. Qed.
Lemma NoDup_fst_filter_map_to_list m : NoDup (filter P (map_to_list m)).*1.
Proof.
apply NoDup_fmap_fst; [| apply NoDup_filter, NoDup_map_to_list ].
intros a b1 b2; do 2 rewrite elem_of_list_filter.
destruct 1 as [HP1 in_map_1]; destruct 1 as [HP2 in_map_2].
by apply (map_to_list_unique m a).
Qed.
Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).
Proof.
apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment