proposition: Lemma disjointU2_rw a b x y: y <> x -> disjointU (variantL x y a b) = (a *s1 x) \cup (b *s1 y).
proof: Proof. move=> yx. rewrite/disjointU /disjointU_fam. have -> : domain (variantL x y a b) = doubleton x y by rewrite/ variantL; aw. set_extens z. move/setUb_P; aw; move => [u ud]; rewrite LgV //; move/setX_P => [pz Pz Qz]. rewrite -pz; move/set1_P: Qz ->; apply/setU2_P; move: Pz. case /set2_P: ud=> ->; rewrite ?variant_V_a ? (variant_V_b _ _ yx); [left | right]; apply: setXp_i => //; fprops. move=> h. have Qz: (inc (Q z) (doubleton x y)). case /setU2_P :h => /setX_P [_ _] /set1_P ->; fprops. apply/setUb_P; aw; exists (Q z) => //; rewrite LgV //. by case/setU2_P: h => /setX_P [pz Pz w]; move/set1_P: (w) ->; apply: setX_i; fprops; rewrite ?variant_V_a ? variant_V_b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)