proposition: Lemma AsAR s t H : aAR (s,t,H) \in As = [&& fAR s t^- \in F & H \in Hs].
proof: Proof. rewrite !inE !eqF //= in_fimset2 // ; last by split; congruence. rewrite ![aAR _]curryE !in_fimset2F // !orbF !inE in_fsetX !negE /=. case e: (fAR _ _^- \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)