proposition: Lemma mutually_disjoint_prop3 D f: mutually_disjoint (Lg D (fun i => f i *s1 i)).
proof: Proof. apply: mutually_disjoint_prop2; move=> u v y _ _. by move=> /setX_P [_ _ /set1_P <-] /setX_P [_ _ /set1_P <-]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)