CoPset finite decomposition into singletons
I'm working with a proof that requires unlimited tokens, which leads me to use the disjoint union CoPset
cmra.
In a specific subproof I need to split a finite set X : gset positive
of tokens into singletons:
own γ (CoPset $ of_gset X) ≡ [∗ set] i ∈ X, own γ (CoPset $ of_gset {[i]})
With big_opS_commute1
I can get
own γ ([⋅ set] i ∈ X, CoPset $ of_gset {[i]}) ≡ [∗ set] i ∈ X, own γ (CoPset $ of_gset {[i]})
And then I only need to show that
CoPset $ of_gset X ≡ [⋅ set] i ∈ X, CoPset $ of_gset {[i]}
,
which currently there seems to be no easy way to solve.
Is there an induction principle for gset's, or any way to solve this?