proposition: Lemma Eqc_disjointU1 X Y: fgraphs_equipotent X Y -> (disjointU X) =c (disjointU Y).
proof: Proof. move=> [pc pd]. apply: Eqc_disjointU; rewrite /fgraphs_equipotent; fprops. split; rewrite/disjointU_fam -? dXY; aww. by move=> i idy; rewrite !LgV//; fprops; try ue; rewrite !Eq_indexed_c pd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)