proposition: Lemma Eqc_disjointU2 a b a' b': disjoint a b -> disjoint a' b' -> a =c a' -> b =c b' -> (a \cup b) =c (a' \cup b').
proof: Proof. move=> dab dab' eqq' ebb'. rewrite ! union2Lv; apply:Eqc_disjointU; try apply: disjointLv =>//. by hnf;saw => // i ind; try_lvariant ind. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)