proposition: Lemma consistentU : consistent (V1 :|: V2) (E1 :|: E2).
proof: Proof. Proof using con1 con2. move => e b. case/setUP => E. - by rewrite !inE con1. - by rewrite !inE con2. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)