fact: Definition sf_closed' (F : {fset sform}) (s:sform) := match s with | (fImp s t,b) => ((s,negb b) \in F) && ((t,b) \in F) | (fAX s, b) => (s,b) \in F | (fAG s, b) => [&& (fAX (fAG s),b) \in F & (s,b) \in F] | _ => true end.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)