fact: Fixpoint nt (u: term): nterm := match u with | tm_dot u v => nt_dot (nt u) (nt v) | tm_par u v => nt_par (nt u) (nt v) | tm_cnv u => nt_cnv (nt u) | tm_var a => nt_var a | tm_dom u => nt_dom (nt u) | tm_one => nt_one end.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures)