proposition: Lemma ax_Req C L : C \in Req L -> prv ([af L] ---> EX [af C]).
proof: Proof. rewrite !inE. case/predU1P => [->|]. - rewrite -> box_request. do 2 Intro. ApplyH ax_serial. Rev. ApplyH axN. Rev. apply: rNorm. exact: axContra. - case/fimsetP => s. rewrite inE. move: s => [[|?|? ?|s|? ?|? ?] [|]] /andP [//=] inL _ ->. rewrite -> andU,(axA2 [af L]). rewrite <- af1n. rewrite -> (bigAE _ inL),box_request at 1. rewrite /=. rule axAcase. rewrite <- (axDN s) at 1. exact: axDBD. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.CTL(CTL_def dags demo hilbert relaxed_pruning)