proposition: Lemma genU_jmp C E : (C,E) \in U -> (R C, aR E) \in U.
proof: Proof. rewrite !in_fsetX /= => /andP [? ?]. rewrite RinU //. exact: genU_aR. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)