proposition: Lemma R1inU C s : C \in U -> fAX s^- \in C -> s^- |` R C \in U.
proof: Proof. Proof using sfc_F. move => CinU inC. rewrite powersetU RinU // powersetE fsub1 andbT. rewrite powersetE in CinU. by move/(subP CinU)/sfc_F : inC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def)