proposition: Lemma Eq_du2 a b a' b' : disjoint a b -> disjoint a' b' -> a \Eq a' -> b \Eq b' -> (a \cup b) \Eq (a' \cup b').
proof: Proof. move => du1 du2 [f [[[ff fi] [_ fs]] sf tf]] [g [[[fg gi] [_ gs]] sg tg]]. pose h x := Yo (inc x a) (Vf f x) (Vf g x). exists (Lf h (a \cup b) (a' \cup b')); saw. rewrite sf in fi fs; rewrite sg in gi gs;rewrite tf in fs; rewrite tg in gs. have Ha x: inc x b -> ~ inc x a by clear du2;move => ba bb; empty_tac1 x. rewrite /h;apply: lf_bijective. - move =>x /setU2_P; case => xa; first by Ytac0; apply:setU2_1; Wtac. move: (Ha x xa) => wb; Ytac0;apply:setU2_2; Wtac. - move => u v; case/setU2_P => ua; case/setU2_P => va. + by Ytac0; Ytac0; apply: fi. + move: (Ha _ va) => wb; Ytac0; Ytac0 => sv. empty_tac1 (Vf f u); [ Wtac | rewrite sv;Wtac]. + move: (Ha _ ua) => wb; Ytac0; Ytac0 => sv. empty_tac1 (Vf g u); [ rewrite sv; Wtac | Wtac]. + by move: (Ha _ ua) (Ha _ va)=> ub bv; Ytac0; Ytac0; apply: gi. move => y /setU2_P; case => ya. by move:(fs _ ya) =>[x xqa ->]; exists x; fprops; Ytac0. by move:(gs _ ya) =>[x xqa ->]; exists x; fprops; rewrite Y_false => //;case/Ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)