proposition: Lemma pblock_eqvE (T : finType) (R : rel T) (D : {set T}) x y : {in D & &, equivalence_rel R} -> y \in pblock (equivalence_partition R D) x -> [/\ x \in D, y \in D & R x y].
proof: Proof. move => eqv_R. move/equivalence_partitionP : (eqv_R) => /and3P [P1 P2 P3]. rewrite /pblock /=. case: pickP => //=; last by rewrite inE. move => B /andP [B1 xB] yB. have H: {subset B <= D}. { move => z zB. rewrite -(eqP P1). by apply/bigcupP; exists B. } rewrite -(pblock_equivalence_partition eqv_R) ?H //. rewrite -eq_pblock ?(def_pblock _ _ xB,def_pblock _ _ yB) //. by apply/bigcupP; exists B. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)