proposition: Lemma genU_aR E : E \in As -> aR E \in As.
proof: Proof. case: E => //=; try by rewrite AsV. case => [[u v] H]. by rewrite AsX. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)