proposition: Lemma supp_lit C s b : literal (s,b) -> supp C s b = ((s,b) \in C).
proof: Proof. by case: s. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)