proposition: Lemma FL_closed u : sf_closed (FL u).
proof: Proof. case => //. - move => s t A /=. apply/andP;split; apply: FL_trans A; by rewrite !inE FL_refl. - case => //= [p s|p1 p2 s|p1 p2 s|p s|s t] A; repeat (apply/andP;split); by [apply: FL_trans A; rewrite !inE ?FL_refl ?FL0_refl ]. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)