fact: Definition tgraph_of_nterm (t: nterm): tgraph2 := match t with | nt_test a => unit_graph2 a | nt_conn a u b => edge_graph2 a u b end.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)