proposition: Lemma decomp_cnv (G : graph2) T D : sdecomp T (sskeleton G) D -> sdecomp T (sskeleton (G°)) D.
proof: Proof. move/sdecomp_sskel => [dec cmp]. apply/sdecomp_sskel; split => //. move: cmp => [t] H. exists t => /=. by rewrite andbC. Qed.
imports: Coq(RelationClasses Setoid) mathcomp(all_ssreflect) GraphTheory(edone set_tac finite_quotient preliminaries) GraphTheory(digraph sgraph treewidth minor equiv setoid_bigop) GraphTheory(structures mgraph pttdom ptt mgraph2 skeleton)