Skip to content
Snippets Groups Projects
Commit 3303ec5e authored by Ralf Jung's avatar Ralf Jung
Browse files

make name more consistent

parent 407d8414
No related branches found
No related tags found
No related merge requests found
...@@ -177,7 +177,7 @@ Qed. ...@@ -177,7 +177,7 @@ Qed.
Lemma size_dom `{!Elements K D, !FinSet K D} {A} (m : M A) : Lemma size_dom `{!Elements K D, !FinSet K D} {A} (m : M A) :
size (dom D m) = size m. size (dom D m) = size m.
Proof. Proof.
rewrite dom_alt, list_to_set_size. rewrite dom_alt, size_list_to_set.
2:{ apply NoDup_fst_map_to_list. } 2:{ apply NoDup_fst_map_to_list. }
unfold size, map_size. rewrite fmap_length. done. unfold size, map_size. rewrite fmap_length. done.
Qed. Qed.
......
...@@ -203,7 +203,7 @@ Proof. ...@@ -203,7 +203,7 @@ Proof.
by apply size_non_empty_iff, non_empty_difference. by apply size_non_empty_iff, non_empty_difference.
Qed. Qed.
Lemma list_to_set_size l : Lemma size_list_to_set l :
NoDup l size (list_to_set (C:=C) l) = length l. NoDup l size (list_to_set (C:=C) l) = length l.
Proof. Proof.
intros Hl. unfold size, set_size. simpl. intros Hl. unfold size, set_size. simpl.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment