proposition: Proposition nt_correct (u: term): u ≡ term_of_nterm (nt u).
proof: Proof. induction u=>//=; fold_ops. - rewrite (dot_eqv _ _ IHu1 _ _ IHu2). case (nt u1) =>[a|a u b]; case (nt u2)=>[c|c v d] //=; rewrite !dotA//. - rewrite (par_eqv _ _ IHu1 _ _ IHu2). case (nt u1)=>[a|a u b]; case (nt u2)=>[c|c v d]=>//=. exact: pardot. apply: parC. exact: par_nontest. - rewrite {1}IHu. case (nt u)=>[a|a v b]=>//=. exact: cnvtst. by rewrite 2!cnvdot dotA !cnvtst. - rewrite {1}IHu. case (nt u)=>[a|a v b]=>//=. exact: domtst. by rewrite -dotA A13 domtst. - by rewrite dotx1 dot1x. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures)