proposition: Lemma redirect_consistent (G : graph2) (H : {set G}) (o : G) : let H' := input |: (o |: H) in consistent H' (edge_set H' :\: edges input input).
proof: Proof. apply: consistent_setD. exact: induced_proof. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)