proposition: Lemma fset1UE (T : choiceType) (x a : T) (A : {fset T}) : x \in a |` A -> (x = a) + (x != a) * (x \in A).
proof: Proof. rewrite !inE. case: (altP (x =P a)) => /=; [by left|by right;split]. Qed.
imports: mathcomp(all_ssreflect)