proposition: Lemma soundness s : prv s -> forall (M:cmodel) (w:M), eval s w.
proof: Proof. elim => {s}. - by [move => /= *; firstorder]. - by [move => /= *; firstorder]. - by [move => /= *; firstorder]. - move => /= s M w H. by case: (modelP s w); firstorder. - by [move => /= *; firstorder]. - by [move => /= *; firstorder]. - by move => s M w [H ?]. - by move => s M w [? H]. - move => u s _ Hstep _ Hs M. cofix soundness => w /= Hw. apply: AGs => [|v wv]; first exact: Hs. apply: soundness. exact: Hstep wv. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)