proposition: Lemma fset2_inv (T : choiceType) (x y x' y' : T) : x != y -> [fset x;y] = [fset x';y'] -> (x = x' /\ y = y') + (x = y' /\ y = x').
proof: Proof. move => /negbTE D /fsetP H. move: (H x). rewrite !inE eqxx /= => /esym. case/orb_sum => /eqP ?;[left|right]; subst; move: (H y). - rewrite !inE eqxx orbT eq_sym D. by move/esym/eqP. - rewrite !inE eqxx orbT [y == y']eq_sym D orbF. by move/esym/eqP. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries)