proposition: Corollary valid_dec s : decidable (forall (M:cmodel) (w:M), eval s w).
proof: Proof. case (sat_dec (fImp s fF)) => /= H;[by firstorder|left => M w]. by case (modelP s w); firstorder. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.K(K_def demo)