proposition: Lemma fclosed1 (a : {pred T}) : fclosed f a -> forall x, (x \in a) = (f x \in a).
proof: Proof. by move=> cl_a x; apply: cl_a (eqxx _). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)