proposition: Lemma glue2_irrefl : irreflexive glue2_rel.
proof: Proof. by move => [u|u] /=; rewrite sgP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)