proposition: Lemma refE1n s C : href (s^- |` C) -> prv ([af C] ---> s).
proof: Proof. move => H. rewrite /href in H. rewrite -> andU,bigA1 in H. Intro. ApplyH axDN. Intro. ApplyH H. by ApplyH axAI. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)