proposition: Lemma sfcU (X Y : {fset sform}) : sf_closed X -> sf_closed Y -> sf_closed (X `|` Y).
proof: Proof. rewrite /sf_closed => /= H1 H2 s. case/fsetUP => [/H1 | /H2] H; apply: sf_closed'_mon H _; auto with fset. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)