proposition: Lemma mutually_disjoint_prop f: (forall i j y, inc i (domain f) -> inc j (domain f) -> inc y (Vg f i) -> inc y (Vg f j) -> i = j) -> mutually_disjoint f.
proof: Proof. move=> hyp i j idf jdf; mdi_tac nij => u ui uj; case: nij; exact: (hyp _ _ u). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)