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. - move => s t u _ /= IH1 _ IH2 M w. elim => {w} - w; first exact: IH1. move => ws H1 H2. exact: IH2. - move => s t M w /=. exact: AU0. - move => s t M w /=. exact: AUs. - move => s t u _ IH1 _ IH2. cofix soundness => /= M w H. case (modelP s w) => Hs. - apply: AR0 Hs _. exact: IH1 H. - apply: ARs. exact: IH1 H. move => v wv. apply: soundness. exact: IH2 wv. - move => s t M w /=. by case. - move => s t M w /=. by case. - move => M w /=. case: (serial w) => v wv. by move/(_ _ wv). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.CTL(CTL_def)