proposition: Lemma soundness s : prv s -> forall (M:cmodel) (w:M), eval s w.
proof: Proof. elim => {s} ; try by [move => /= *; firstorder]. move => /= s M w H. by case: (modelP s w); firstorder. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)