proposition: Lemma Eqc_disjointU X Y: fgraphs_equipotent X Y -> mutually_disjoint X -> mutually_disjoint Y -> (unionb X) =c (unionb Y).
proof: Proof. move=> [dXY ale] mX mY. pose g i := equipotent_ex (Vg X i) (Vg Y i). set X' := (Lg (domain X) (Vg X)). have pfX: partition_w_fam X' (unionb X). rewrite /X';split; fprops. by hnf; aw; move => a b ax bx; rewrite !LgV //; apply: mX. by rewrite (unionb_gr X). pose h i := triple (source (g i)) (unionb Y) (graph (g i)). have fph: forall i, inc i (domain X')-> function_prop (h i)(Vg X' i) (unionb Y). rewrite /X'; aw; move=> i idx; aw. move: (equipotent_ex_pr1 (ale _ idx)) => [[[fg _] _] sg tg]. hnf;rewrite /h; aw; rewrite LgV //; split => //. apply: function_pr; fprops. apply: (@sub_trans (target (g i))). by apply: f_range_graph. rewrite tg; move=> t tf; union_tac; ue. by rewrite domain_fg. move:(extension_partition1 pfX fph). set x := common_ext _ _ _;move=> [[fx sx tx] agx']. have agx:forall i, inc i (domain X) -> agrees_on (Vg X i) x (h i). by move: agx'; rewrite /X';aw => h1 i idx; move: (h1 _ idx); rewrite LgV. apply/card_eqP; exists x; split => //. split; split=>//. rewrite sx;move=> a b /setUb_P [i idX ai] /setUb_P [j jdX bj]. have ->: Vf x a = Vf (g i) a. by move:(agx _ idX) => [_ _ ha];rewrite (ha _ ai) /Vf /h; aw. have ->: Vf x b = Vf (g j) b. by move:(agx _ jdX) => [_ _ hb];rewrite (hb _ bj) /Vf /h; aw. move: (equipotent_ex_pr1 (ale _ idX)) => [[[fg ig] _] sg tg]. move: (equipotent_ex_pr1 (ale _ jdX)) => [[[fg' _] _] sg' tg']. have Wta: (inc (Vf (g i) a) (Vg Y i)) by rewrite -tg /g ; Wtac. have Wtb: (inc (Vf (g j) b) (Vg Y j)) by rewrite - tg' /g; Wtac. rewrite dXY in idX jdX. case: (mY _ _ idX jdX) => eq. rewrite -eq in bj |- * ; apply: ig; ue. move=> eq'; rewrite -eq' in Wtb. by red in eq;empty_tac1 (Vf (g i) a ). rewrite tx=> y /setUb_P; rewrite -dXY; move=> [i idX yV]. move: (equipotent_ex_pr1 (ale _ idX)) => [[_ sg] srg tg]. rewrite -tg in yV; move: ((proj2 sg) _ yV) => [z zsg Wg]. move: (agx _ idX)=> [s1 s2 v]. exists z; first by apply: s1; ue. by rewrite srg in zsg; rewrite v// Wg /Vf /h; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)