proposition: Theorem graph_of_TW2 (u : term A) : exists T D, [/\ @sdecomp T (sskeleton (graph_of_term u)) D & width D <= 3].
proof: Proof. apply eval_TW2 => a. apply: decomp_small. by rewrite card_sum card_unit. 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)