proposition: Lemma in_fsep (T : choiceType) (A : {fset T}) (P : pred T) (y : T) : y \in [fset x | x in A & P x] = (y \in A) && (P y).
proof: Proof. apply/imfsetP/andP => /= [[x]|[H1 H2]]; first by rewrite inE => /andP[H1 H2] ->. exists y => //. by rewrite inE H1. Qed.
imports: mathcomp(all_ssreflect)