proposition: Lemma plainP C u E : step_plain_cases (fset.lfp U step) C u E -> (u |` C,E) \in U -> step_plain (fset.lfp U step) (u |` C,E).
proof: Proof. move => H. rewrite in_fsetX powersetU powersetE fsub1 -andbA -/Cs. case/and3P => ? ? ?. apply/hasP; exists u => //. apply/hasP; exists C => //. apply/hasP; exists E => //. by rewrite eqxx. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)