proposition: Lemma AsAU s t H : aAU (s,t,H) \in As = [&& fAU s t^+ \in F & H \in Hs].
proof: Proof. rewrite !inE !eqF //= in_fimset2 // ; last by split; congruence. rewrite ![aAU _]curryE !in_fimset2F // !orbF !inE in_fsetX !posE /=. case e: (fAU _ _^+ \in F) => //. by case/and3P:(sfc_F e) => _ -> ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)