proposition: Lemma sfc_ssub s : sf_closed (ssub s).
proof: Proof. case: s. elim => [|x|s IHs t IHt|s IHs|s IHs t IHt|s IHs t IHt] b //= u; rewrite !inE ?orbF. - by move/eqP => -> /=. - by move/eqP => -> /=. - case/orP => [/eqP ->|H] /=. by rewrite !inE !ssub'_refl. apply: sf_closed'_mon (fsubUr _ _). case/orP: H => H. apply: sf_closed'_mon (fsubUl _ _). exact: IHs. apply: sf_closed'_mon (fsubUr _ _). exact: IHt. - case/orP => [/eqP ->|H] /=. by rewrite !inE !ssub'_refl. apply: sf_closed'_mon (fsubUr _ _). exact: IHs. - case/or3P => [/eqP ->| /eqP -> | H] /=; try by rewrite !inE ?ssub'_refl. do 2 apply: sf_closed'_mon (fsubUr _ _). case/orP : H => H. apply: sf_closed'_mon (fsubUl _ _). exact: IHs. apply: sf_closed'_mon (fsubUr _ _). exact: IHt. - case/or3P => [/eqP ->| /eqP -> | H] /=; try by rewrite !inE ?ssub'_refl. do 2 apply: sf_closed'_mon (fsubUr _ _). case/orP : H => H. apply: sf_closed'_mon (fsubUl _ _). exact: IHs. apply: sf_closed'_mon (fsubUr _ _). exact: IHt. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)