proposition: Lemma plain_inU {C} : (C,aVoid) \in U (sfc C).
proof: Proof. by rewrite in_fsetX !inE //= andbT powersetE sub_sfc. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)