proposition: Lemma CK4F_split_cpM : CK4F (@bgraph _ _ G IO z).
proof: Proof. apply rec_bag => //. apply/bigcupP. exists (input,output) => //. 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)