fact: Definition sat (M:cmodel) C := exists (w:M), forall s, s \in C -> eval (interp s) w.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)