theorem finset_union_left_cancel {V : Type} [DecidableEq V] {σ C D : Finset V} (hC_disj : Disjoint σ C) (hD_disj : Disjoint σ D) (h_eq : σ ∪ C = σ ∪ D) : C = D

Left-cancellation for finite unions disjoint from $\sigma$: if $\sigma \cup C = \sigma \cup D$ with both $C$ and $D$ disjoint from $\sigma$, then $C = D$.