proposition: Lemma term_of_rec_eq' (f g : graph2 -> term sym) (G : graph2) : (forall H : graph2, #|H| < #|G| -> f H = g H) -> term_of_rec' f G = term_of_rec' g G.
proof: Proof. move => Efg. rewrite /term_of_rec'. case: pickP => [x /andP [X1 X2]|//]. rewrite Efg //. exact: induced2_compN_small. Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries set_tac) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(equiv setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 ptt mgraph2_tw2 skeleton) GraphTheory(bounded extraction_def extraction_iso excluded)