proposition: Lemma suppCWL L1 L2 C : suppC L2 C -> suppC (L1 `|` L2) C.
proof: Proof. apply: sub_all => s. apply: supp_mon; auto with fset. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert)