Implement suggestions by Robbert Krebbers on gmap.

parent 750d8f52
Pipeline #19058 canceled with stage
......@@ -282,9 +282,9 @@ Section gset.
Lemma dom_gset_to_gmap {A} (X : gset K) (x : A) :
dom _ (gset_to_gmap x X) = X.
Proof.
revert X; apply set_ind_L; [|intros y X not_in_m dom_eq];
[rewrite gset_to_gmap_empty, dom_empty_L|
rewrite gset_to_gmap_union_singleton, dom_insert_L, dom_eq]; done.
induction X as [| y X not_in IH] using set_ind_L.
- rewrite gset_to_gmap_empty, dom_empty_L; done.
- rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done.
Qed.
End gset.
......
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