proposition: Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (.≡ ∅) Xs.
proof: Proof. split. - induction Xs; simpl; rewrite ?empty_union; intuition. - induction 1 as [|?? E1 ? E2]; simpl; [done|]. by apply empty_union. Qed.
imports: stdpp(finite) stdpp(options)