proposition: Lemma union_list_reverse Xs : ⋃ (reverse Xs) ≡ ⋃ Xs.
proof: Proof. induction Xs as [|X Xs IH]; simpl; [done |]. by rewrite reverse_cons, union_list_app, union_list_singleton, (comm _), IH. Qed.
imports: stdpp(finite) stdpp(options)