proposition: Lemma evalP2 (M:fmodel) s (w : M) : satisfies s w <-> eval s w.
proof: Proof. apply: rwP2 (evalP w s). elim: s w => [|x|s IHs t IHt|s IHs|s IHs t IHt|s IHs t IHt] w /=. - by constructor. - exact: idP. - apply: iffP (@implyP _ _) _ _ => ? /IHs ?; apply/IHt; firstorder. - apply: iffP (@forall_inP _ _ _) _ _ => H v /H /IHs; done. - apply: iffP (@arP2 _ _ _ _ _ _ ) _ _; first exact: fser; apply: pAR_strengthen; intuition; solve [exact/IHs|exact/IHt]. - apply: iffP (@auP2 _ _ _ _ _ _ ) _ _;first exact: fser; apply: pAU_strengthen; intuition; solve [exact/IHs|exact/IHt]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)