proposition: Lemma partition_setU2 A B (f: fterm): disjoint A B -> partition_w_fam (variantLc A B) (domain (Lg (A \cup B) f)).
proof: Proof. aw; hnf; rewrite union2Lv;split; fprops. move => i j; aw; case/C2_P => ->; case/C2_P => ->; aww. by right; apply: disjoint_S. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)