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