proposition: Lemma disjointU_disjoint f: mutually_disjoint (disjointU_fam f).
proof: Proof. move=> i j; rewrite Lgd=> id jd ;rewrite ! LgV //. by mdi_tac t => u /indexed_P [_ _] qu /indexed_P [_ _]; rewrite qu. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)