proposition: Fact redirect_output_proof (T : finType) x y (B : {set T}) : x \in y |: (x |: B).
proof: Proof. by rewrite !inE eqxx. 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)