proposition: Lemma suppxx C : literalC C -> suppC C C.
proof: Proof. move/allP => lit_C. apply/allP => [[s b]] /= inC. rewrite /supp supp_lit //. exact: lit_C. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert)