proposition: Lemma genU_ipl s t C E : (fImp s t^+ |` C, E) \in U -> (s^- |` C, E) \in U.
proof: Proof. apply: subU => /=. auto with fset. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)