proposition: Lemma iso_K4_free (G H : sgraph) : diso G H -> K4_free H -> K4_free G.
proof: Proof. move => iso_GH. apply: subgraph_K4_free. exact: iso_subgraph. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)