Skip to content
Snippets Groups Projects
Verified Commit 76bc1683 authored by Dorian Lesbre's avatar Dorian Lesbre
Browse files

Fix pipeline

parent d1dfd1ae
Branches
No related tags found
1 merge request!444Add images (codomains) to finite maps
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
stdpp/fin_map_img.v
+ 1
− 1
View file @ 76bc1683
......@@ -154,7 +154,7 @@ Section fin_map_img.
Proof.
induction m using map_ind.
- rewrite img_empty. apply empty_finite.
- apply (set_finite_subseteq _ _ (img_insert i x m)).
- apply (set_finite_subseteq _ _ (img_insert _ _ m)).
apply union_finite; [ apply singleton_finite | apply IHm ].
Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment