proposition: Lemma tgraph_graph (u: term): tgraph_of_term u ≃2 relabel2 (fun _ => 1%CM) (fun x : flat A => pttdom.tm_var x) (graph_of_term u).
proof: Proof. have ? : 1%CM ≡ (1 ⊗ 1)%CM by move => M; rewrite monU. induction u=>/=. - etransitivity. apply (dot_iso2 IHu1 IHu2). symmetry. apply relabel2_dot => //. - etransitivity. apply (par_iso2 IHu1 IHu2). symmetry. apply relabel2_par=>//. - etransitivity. apply (cnv_iso2 IHu). symmetry. apply relabel2_cnv=>//. - etransitivity. apply (dom_iso2 IHu). symmetry. apply relabel2_dom=>//. - symmetry. apply relabel2_one=>//. - symmetry. apply relabel2_var=>//. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) GraphTheory(setoid_bigop structures mgraph pttdom mgraph2) GraphTheory(rewriting reduction open_confluence transfer)