proposition: Lemma decomp_iso (G1 G2 : sgraph) (T : forest) B1 : sdecomp T G1 B1 -> diso G1 G2 -> exists2 B2, sdecomp T G2 B2 & width B2 = width B1.
proof: Proof. case => D1 D2 D3 [[g f can_g can_f] /= hom_g hom_f]. exists (fun t => [set g x | x in B1 t]). - split. + move => x. case: (D1 (f x)) => t Ht. exists t. apply/imsetP. by exists (f x). + move => x y /hom_f /D2 [t] /andP [t1 t2]. exists t. by rewrite -[x]can_f -[y]can_f !imset_f. + move => x t1 t2 /imsetP [x1] X1 ? /imsetP [x2] X2 P. subst. have ?: x1 = x2 by rewrite -[x1]can_g P can_g. subst => {P}. have := D3 _ _ _ X1 X2. apply: connect_mono => t t' /=. rewrite !inE -andbA => /and3P [A B ->]. by rewrite !imset_f. - rewrite /width. apply: eq_bigr => i _. rewrite card_imset //. apply: can_inj can_g. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)