proposition: Lemma soundness s: prv s -> valid s.
proof: Proof. elim => {s}; try by move => *; firstorder. - move => s t _ A _ B M w. apply: A. exact: B. - move => s M v /=. exact: modelP. - move => p s M v /=. apply. by constructor. - move => p s M v H u vRu w uRw /=. apply: H. exact: StarL. - move => p u _ IHu M v H w /= vRw. elim: vRw H => // {v w} - v w ? vRu _ IH H. apply: IH. exact: IHu. - by move => s t M v /= A w [->]. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)