fact: Definition nt_cnv u := match u with | nt_test _ => u | nt_conn a u b => nt_conn b (u°) a end.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures)