proposition: Lemma set_pred0 (T : finType) : @set0 T =i pred0.
proof: Proof. move => z. by rewrite !inE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph minor) GraphTheory(checkpoint connectivity excluded set_tac)