proposition: Lemma disjointLv a b: disjoint a b -> mutually_disjoint (variantLc a b).
proof: Proof. move=> db i j; aw => id1 jd; try_lvariant id1; try_lvariant jd; fprops. by right;apply:disjoint_S. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)