proposition: Lemma skel_K4_free (u : term A) : K4_free (skeleton (graph_of_term u)).
proof: Proof. apply: minor_K4_free (@sskel_K4_free u). exact: sub_minor (skel_sub _). 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)