proposition: Lemma disjointU_E I (f:fterm ): disjointU (Lg I f) = unionf I (fun i : Set => f i *s1 i).
proof: Proof. rewrite /disjointU/disjointU_fam/unionb; aw. by apply: setUf_exten => i iI; rewrite !LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)