proposition: Lemma smerge2_irrefl : irreflexive smerge2_rel.
proof: Proof. by move => u /=; case: (sval u == x); rewrite /= ?andbF ?sgP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)