proposition: Lemma sskel_K4_free (u : term A) : K4_free (sskeleton (graph_of_term u)).
proof: Proof. case: (graph_of_TW2 u) => T [B] [B1 B2]. exact: TW2_K4_free B1 B2. 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)