proposition: Lemma tgraph_graph_iso (u v: term): graph_of_term u ≃2p graph_of_term v -> tgraph_of_term u ≃2p tgraph_of_term v.
proof: Proof. intros [h]. exists. etransitivity. apply tgraph_graph. etransitivity. 2: symmetry; apply tgraph_graph. apply relabel2_iso=>//. case=>//=??/=->//. 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)