proposition: Lemma decomp_iso2 (G1 G2 : graph2) (T : forest) B1 : @sdecomp T (sskeleton G1) B1 -> G1 ≃2 G2 -> exists2 B2, @sdecomp T (sskeleton G2) B2 & width B2 = width B1.
proof: Proof. move => dec iso. apply: decomp_iso dec _. exact: sskel_iso2. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)