proposition: Lemma sts_agreement (M:sts) (w :M) s : eval s w <-> satisfies s w.
proof: Proof. Proof using xm dc. elim: s w => //= [s IHs t IH|s IHs|s IHs t IH|s IHs t IH] w. - firstorder. - firstorder. - split => H. + apply: (AR2 xm). apply: AR_strengthen H => *; by firstorder. + apply: (AR1 (@serial M) xm (@dc M)). apply: pAR_strengthen H => *; by firstorder. - split => H. + apply: AU1. apply: AU_strengthen H => *; by firstorder. + apply: (AU2 (@serial M) xm (@dc M)). apply: pAU_strengthen H => *; by firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)