proposition: Lemma term_of_eq : forall (G : graph2), CK4F G -> term_of G = term_of_rec term_of G.
proof: Proof. apply: Fix_eq term_of_rec_eq. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)