fact: Definition sf_closed' (F : {fset form}) s := match s with | fImp s t => (s \in F) && (t \in F) | [pV _]s => s \in F | [p0;;p1]s => [&& [p0][p1]s \in F, [p1]s \in F & s \in F] | [p0 + p1]s => [&& [p0]s \in F, [p1]s \in F & s \in F] | [p^*]s => ([p][p^*]s \in F) && (s \in F) | [s??]t => (s \in F) && (t \in F) | [p^^]s => ([p]s \in F) && (s \in F) | _ => true end.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)